Lines Matching defs:constructors
1564 (* constructors determined by applying the function is complete, ie. *)
1565 (* contains all the constructors for that type: *)
1567 (* Notes: All arguments to constructors must be free variables *)
1577 (* --> For a type with n constructors should have n clauses *)
1603 (* constructors are processed. Eg. *)
1608 (* If the list given does not correctly split the constructors then *)
1744 let val constructors = map (fn x => outermost (mk_eq (x,x))) missing
1747 (case (mk_set (map (base_type o type_of) constructors))
1750 "Types of constructors do not match!")
1752 if all (all is_var o snd o strip_comb) constructors andalso
1754 constructors) (constructors_of x)
1755 then let val var = case (total (tryfind (hd o free_vars)) constructors)
1761 in [subst (map (fn c => c |-> var) constructors) (hd missing)]
1776 "Two or more function clauses do not differ by constructors")
2073 (* Returns a theorem that resolves nested constructors: *)
2084 (mkDebugExn "mk_initial" "Invalid list of constructors")
2364 val constructors = constructors_of t handle e =>
2370 (enumerate 0 (fst (strip_fun (type_of c))))) constructors;
2373 vars constructors
2377 (enumerate 0 constructors) vars) handle e => wrap e
2391 case_defs3) constructors
2501 (* Add rewrites to encode constructors, case theorems, and encoding of *)
3000 let val (fconst,constructors) = strip_comb missing
3001 val fvs = free_varsl constructors
3002 val arg_names = map (implode o base26 o fst) (enumerate 0 constructors)
3004 arg_names constructors
3008 (zip args constructors)
3013 " has no constructors."))
3162 (* of constructors, rather than their absense, eg.: *)
3164 (* 5) Generation of extra limit theorems for nested constructors *)