equal
deleted
inserted
replaced
37 val pprint_typ: sg -> typ -> pprint_args -> unit |
37 val pprint_typ: sg -> typ -> pprint_args -> unit |
38 val certify_typ: sg -> typ -> typ |
38 val certify_typ: sg -> typ -> typ |
39 val certify_term: sg -> term -> term * typ * int |
39 val certify_term: sg -> term -> term * typ * int |
40 val read_typ: sg * (indexname -> sort option) -> string -> typ |
40 val read_typ: sg * (indexname -> sort option) -> string -> typ |
41 val infer_types: sg -> (indexname -> typ option) -> |
41 val infer_types: sg -> (indexname -> typ option) -> |
42 (indexname -> sort option) -> string list -> bool -> bool |
42 (indexname -> sort option) -> string list -> bool |
43 -> term list * typ -> int * term * (indexname * typ) list |
43 -> term list * typ -> int * term * (indexname * typ) list |
44 val add_classes: (class * class list) list -> sg -> sg |
44 val add_classes: (class * class list) list -> sg -> sg |
45 val add_classrel: (class * class) list -> sg -> sg |
45 val add_classrel: (class * class) list -> sg -> sg |
46 val add_defsort: sort -> sg -> sg |
46 val add_defsort: sort -> sg -> sg |
47 val add_types: (string * int * mixfix) list -> sg -> sg |
47 val add_types: (string * int * mixfix) list -> sg -> sg |
250 |
250 |
251 |
251 |
252 |
252 |
253 (** infer_types **) (*exception ERROR*) |
253 (** infer_types **) (*exception ERROR*) |
254 |
254 |
255 fun infer_types sg types sorts used freeze print_msg (ts, T) = |
255 fun infer_types sg types sorts used freeze (ts, T) = |
256 let |
256 let |
257 val Sg {tsig, ...} = sg; |
257 val Sg {tsig, ...} = sg; |
258 val show_typ = string_of_typ sg; |
258 val show_typ = string_of_typ sg; |
259 val show_term = string_of_term sg; |
259 val show_term = string_of_term sg; |
260 |
260 |