1signature pairSyntax = 2sig 3 include Abbrev 4 5 val mk_prod : hol_type * hol_type -> hol_type 6 val dest_prod : hol_type -> hol_type * hol_type 7 val list_mk_prod : hol_type list -> hol_type 8 val strip_prod : hol_type -> hol_type list 9 val spine_prod : hol_type -> hol_type list 10 11 val comma_tm : term 12 val fst_tm : term 13 val snd_tm : term 14 val swap_tm : term 15 val uncurry_tm : term 16 val curry_tm : term 17 val pair_map_tm : term 18 val lex_tm : term 19 val pair_case_tm : term 20 21 val mk_pair : term * term -> term 22 val mk_fst : term -> term 23 val mk_snd : term -> term 24 val mk_swap : term -> term 25 val mk_curry : term * term * term -> term 26 val mk_uncurry : term * term -> term 27 val mk_pair_map : term * term -> term 28 val mk_lex : term * term -> term 29 val mk_pabs : term * term -> term 30 val mk_pforall : term * term -> term 31 val mk_pexists : term * term -> term 32 val mk_pexists1 : term * term -> term 33 val mk_pselect : term * term -> term 34 val mk_plet : term * term * term -> term 35 val mk_anylet : (term * term) list * term -> term 36 val mk_pair_case : {pairtm : term, ftm : term} -> term 37 38 val dest_pair : term -> term * term 39 val dest_fst : term -> term 40 val dest_snd : term -> term 41 val dest_swap : term -> term 42 val dest_curry : term -> term * term * term 43 val dest_uncurry : term -> term * term 44 val dest_pair_map : term -> term * term 45 val dest_lex : term -> term * term 46 val dest_pabs : term -> term * term 47 val pbvar : term -> term 48 val pbody : term -> term 49 val dest_plet : term -> term * term * term 50 val dest_anylet : term -> (term * term) list * term 51 val dest_pforall : term -> term * term 52 val dest_pexists : term -> term * term 53 val dest_pexists1 : term -> term * term 54 val dest_pselect : term -> term * term 55 val dest_pbinder : term -> exn -> term -> term * term 56 val dest_pair_case : term -> {pairtm : term, ftm: term} 57 58 59 val list_mk_pair : term list -> term 60 val list_mk_pabs : term list * term -> term 61 val list_mk_anylet : (term * term) list list * term -> term 62 val list_mk_pforall : term list * term -> term 63 val list_mk_pexists : term list * term -> term 64 val strip_pair : term -> term list 65 val spine_pair : term -> term list 66 val unstrip_pair : hol_type -> term list -> term * term list 67 val strip_pabs : term -> term list * term 68 val strip_anylet : term -> (term * term) list list * term 69 val strip_pforall : term -> term list * term 70 val strip_pexists : term -> term list * term 71 72 73 val is_pair : term -> bool 74 val is_pair_case : term -> bool 75 val is_fst : term -> bool 76 val is_snd : term -> bool 77 val is_swap : term -> bool 78 val is_curry : term -> bool 79 val is_uncurry : term -> bool 80 val is_pair_map : term -> bool 81 val is_lex : term -> bool 82 val is_pabs : term -> bool 83 val is_plet : term -> bool 84 val is_pforall : term -> bool 85 val is_pexists : term -> bool 86 val is_pexists1 : term -> bool 87 val is_pselect : term -> bool 88 val is_vstruct : term -> bool 89 90 val genvarstruct : hol_type -> term 91 92 val lift_prod : hol_type -> ('a -> term ) -> ('b -> term) 93 -> 'a * 'b -> term 94end 95