1signature fcpSyntax =
2sig
3    include Abbrev
4
5    val mk_numeric_type       : Arbnum.num -> hol_type
6    val mk_int_numeric_type   : int -> hol_type
7    val mk_cart_type          : hol_type * hol_type -> hol_type
8
9    val dest_numeric_type     : hol_type -> Arbnum.num
10    val dest_int_numeric_type : hol_type -> int
11    val dest_cart_type        : hol_type -> hol_type * hol_type
12
13    val is_numeric_type       : hol_type -> bool
14    val is_cart_type          : hol_type -> bool
15
16    val dim_of                : term -> hol_type
17
18    val fcp_tm                : term
19    val fcp_index_tm          : term
20    val dimindex_tm           : term
21    val fcp_update_tm         : term
22    val fcp_hd_tm             : term
23    val fcp_tl_tm             : term
24    val fcp_cons_tm           : term
25    val fcp_map_tm            : term
26    val fcp_exists_tm         : term
27    val fcp_every_tm          : term
28    val v2l_tm                : term
29    val l2v_tm                : term
30
31    val mk_fcp                : term * hol_type -> term
32    val mk_fcp_index          : term * term -> term
33    val mk_dimindex           : hol_type -> term
34    val mk_fcp_update         : term * term * term -> term  (* A[i] := v is mk_fcp_update (A,i,v)  *)
35    val mk_fcp_hd             : term -> term
36    val mk_fcp_tl             : term -> term
37    val mk_fcp_cons           : term * term -> term
38    val mk_fcp_map            : term * term -> term
39    val mk_fcp_exists         : term * term -> term
40    val mk_fcp_every          : term * term -> term
41    val mk_v2l                : term -> term
42    val mk_l2v                : term -> term
43
44    val dest_fcp              : term -> term * hol_type
45    val dest_fcp_index        : term -> term * term
46    val dest_dimindex         : term -> hol_type
47    val dest_fcp_update       : term -> term * term * term
48    val dest_fcp_hd           : term -> term
49    val dest_fcp_tl           : term -> term
50    val dest_fcp_cons         : term -> term * term
51    val dest_fcp_map          : term -> term * term
52    val dest_fcp_exists       : term -> term * term
53    val dest_fcp_every        : term -> term * term
54    val dest_v2l              : term -> term
55    val dest_l2v              : term -> term
56
57    val is_fcp                : term -> bool
58    val is_fcp_index          : term -> bool
59    val is_dimindex           : term -> bool
60    val is_fcp_update         : term -> bool
61    val is_fcp_hd             : term -> bool
62    val is_fcp_tl             : term -> bool
63    val is_fcp_cons           : term -> bool
64    val is_fcp_map            : term -> bool
65    val is_fcp_exists         : term -> bool
66    val is_fcp_every          : term -> bool
67    val is_v2l                : term -> bool
68    val is_l2v                : term -> bool
69
70end
71