Lines Matching defs:constructor
1542 (* Groups clauses to lists matching the outer most left most constructor *)
1543 (* The function supplied strips the constructor out of the term *)
1575 (* 0. Group function clauses by the leftmost outermost constructor. *)
1580 (* constructor in question, in left to right fashion. *)
1585 (* When grouping by constructor, a function term is instantiated to *)
1586 (* match the constructor in use to be passed to the recursive call. *)
1589 (* at the left most outermost constructor. *)
1591 (* If the grouping by constructor procedure returns an empty group *)
2068 (* Returns a polytypic rewrite that converts a nested constructor: *)
2088 val constructor = hd cs
2089 val vars = snd (strip_comb constructor)
2094 val t = type_of constructor
2096 val left = mk_eq(arg,constructor)
2098 map (subst [constructor |-> arg] o concl) normalized)));
2123 let val na = mkStandardExn name "Not a nested constructor"
2429 (* Propagation theorem for a case constructor for a single constructor. *)
2655 "Not an encoded constructor");