1signature FinalType = 2sig 3 4 eqtype hol_type 5 6 val mk_vartype : string -> hol_type 7 val gen_tyvar : unit -> hol_type 8 val dest_vartype : hol_type -> string 9 val is_vartype : hol_type -> bool 10 val is_gen_tyvar : hol_type -> bool 11 12 val mk_type : string * hol_type list -> hol_type 13 val dest_type : hol_type -> string * hol_type list 14 val is_type : hol_type -> bool 15 val mk_thy_type : {Thy:string, Tyop:string, Args:hol_type list} -> hol_type 16 val dest_thy_type : hol_type -> {Thy:string, Tyop:string, Args:hol_type list} 17 18 val decls : string -> {Thy:string, Tyop:string} list 19 val op_arity : {Thy:string, Tyop:string} -> int option 20 21 val type_vars : hol_type -> hol_type list 22 val type_varsl : hol_type list -> hol_type list 23 val type_var_in : hol_type -> hol_type -> bool 24 val exists_tyvar : (hol_type -> bool) -> hol_type -> bool 25 val polymorphic : hol_type -> bool 26 val compare : hol_type * hol_type -> order 27 28 val --> : hol_type * hol_type -> hol_type (* infixr 3 --> *) 29 val dom_rng : hol_type -> hol_type * hol_type (* inverts --> *) 30 val bool : hol_type 31 val ind : hol_type 32 val alpha : hol_type 33 val beta : hol_type 34 val gamma : hol_type 35 val delta : hol_type 36 val etyvar : hol_type 37 val ftyvar : hol_type 38 39 val type_subst : (hol_type,hol_type) Lib.subst -> hol_type -> hol_type 40 41 val match_type : hol_type -> hol_type -> (hol_type,hol_type) Lib.subst 42 43 val match_type_restr : hol_type list -> hol_type -> hol_type 44 -> (hol_type,hol_type) Lib.subst 45 46 val match_type_in_context : hol_type -> hol_type 47 -> (hol_type,hol_type)Lib.subst 48 -> (hol_type,hol_type)Lib.subst 49 val raw_match_type: hol_type -> hol_type 50 -> (hol_type,hol_type) Lib.subst * hol_type list 51 -> (hol_type,hol_type) Lib.subst * hol_type list 52 53 val type_size : hol_type -> int 54 55 val ty_sub : (hol_type,hol_type) Lib.subst -> hol_type -> 56 hol_type Lib.delta 57 58 59 (* accessing and manipulating theory information for types *) 60 val prim_new_type : {Thy:string, Tyop:string} -> int -> unit 61 val prim_delete_type : {Thy:string, Tyop:string} -> unit 62 val thy_types : string -> (string * int) list 63 val del_segment : string -> unit 64 val uptodate_type : hol_type -> bool 65 66 67 68end 69