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