equal
deleted
inserted
replaced
78 val mk_full_horn: (string * typ) list -> term list -> term -> term |
78 val mk_full_horn: (string * typ) list -> term list -> term -> term |
79 |
79 |
80 (* datatype operations *) |
80 (* datatype operations *) |
81 type cns_info = (term * typ * typ list * bool list) list |
81 type cns_info = (term * typ * typ list * bool list) list |
82 |
82 |
83 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
|
84 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
83 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
85 |
84 |
86 (* tactics for function package *) |
85 (* tactics for function package *) |
87 val size_simpset: simpset |
86 val size_simpset: simpset |
88 val pat_completeness_simp: thm list -> Proof.context -> tactic |
87 val pat_completeness_simp: thm list -> Proof.context -> tactic |
307 (* - term for constructor constant |
306 (* - term for constructor constant |
308 - type of the constructor |
307 - type of the constructor |
309 - types of the arguments |
308 - types of the arguments |
310 - flags indicating whether the argument is recursive |
309 - flags indicating whether the argument is recursive |
311 *) |
310 *) |
312 |
|
313 (* returns the type of the nth datatype *) |
|
314 fun all_dtyps descr sorts = |
|
315 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
|
316 |
311 |
317 (* returns info about constructors in a datatype *) |
312 (* returns info about constructors in a datatype *) |
318 fun all_dtyp_constrs_info descr = |
313 fun all_dtyp_constrs_info descr = |
319 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
314 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
320 |
315 |