1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/comp.ma".
24 include "common/prod.ma".
26 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
28 nrecord comparable_ext : Type[1] ≝
30 comp_base : comparable;
31 ltc : (carr comp_base) → (carr comp_base) → bool;
32 lec : (carr comp_base) → (carr comp_base) → bool;
33 gtc : (carr comp_base) → (carr comp_base) → bool;
34 gec : (carr comp_base) → (carr comp_base) → bool;
35 andc : (carr comp_base) → (carr comp_base) → (carr comp_base);
36 orc : (carr comp_base) → (carr comp_base) → (carr comp_base);
37 xorc : (carr comp_base) → (carr comp_base) → (carr comp_base);
38 getMSBc : (carr comp_base) → bool;
39 setMSBc : (carr comp_base) → (carr comp_base);
40 clrMSBc : (carr comp_base) → (carr comp_base);
41 getLSBc : (carr comp_base) → bool;
42 setLSBc : (carr comp_base) → (carr comp_base);
43 clrLSBc : (carr comp_base) → (carr comp_base);
44 rcrc : bool → (carr comp_base) → ProdT bool (carr comp_base);
45 shrc : (carr comp_base) → ProdT bool (carr comp_base);
46 rorc : (carr comp_base) → (carr comp_base);
47 rclc : bool → (carr comp_base) → ProdT bool (carr comp_base);
48 shlc : (carr comp_base) → ProdT bool (carr comp_base);
49 rolc : (carr comp_base) → (carr comp_base);
50 notc : (carr comp_base) → (carr comp_base);
51 plusc_dc_dc : bool → (carr comp_base) → (carr comp_base) → ProdT bool (carr comp_base);
52 plusc_d_dc : (carr comp_base) → (carr comp_base) → ProdT bool (carr comp_base);
53 plusc_dc_d : bool → (carr comp_base) → (carr comp_base) → (carr comp_base);
54 plusc_d_d : (carr comp_base) → (carr comp_base) → (carr comp_base);
55 plusc_dc_c : bool → (carr comp_base) → (carr comp_base) → bool;
56 plusc_d_c : (carr comp_base) → (carr comp_base) → bool;
57 predc : (carr comp_base) → (carr comp_base);
58 succc : (carr comp_base) → (carr comp_base);
59 complc : (carr comp_base) → (carr comp_base);
60 absc : (carr comp_base) → (carr comp_base);
61 inrangec : (carr comp_base) → (carr comp_base) → (carr comp_base) → bool