Lines Matching defs:constructor
10 (* A constructor is a combination of a term with
12 type constructor
14 (* [mk_constructor c arg_names] generate a constructor [c]
16 val mk_constructor : term -> string list -> constructor
18 (* check whether a constructor has no arguments *)
19 val constructor_is_const : constructor -> bool
27 val mk_constructor_term : term list -> constructor -> (term * term list)
28 (* [match_constructor constr t] tries destruct [t] as a constructor
30 the main constructor functions + labelled args. *)
31 val match_constructor : constructor -> term ->
40 of the type can be constructed via a constructor in this list *)
41 val mk_constructorList : bool -> constructor list -> constructorList
53 (* a constructor family is a list of constructors,
57 (* Get the rewrites stored in a constructor family, these
62 (* Get the case-cong stored in a constructor family. *)
66 in a constructor family. *)
72 (* If the constructor family is exhaustive, a theorem stating
81 make a new constructor family. It consists of the constructors
88 proof obligations that occur when creating a new constructor family
96 (* [constructorFamily_of_typebase ty] extracts the constructor family
105 (* A compile database combines constructor families,
144 if no constructor family is found for this column. *)
188 (* add a constructor family to default db *)