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