Lines Matching defs:types
31 (* monomorphic types, but this is not currently done. *)
48 (* they require the theorem for simple types, and don't perform many *)
1897 val types = for 0 (foldl op+ 0 terms)
1899 val vars = map2 (curry mk_var) names types handle e => wrap e
1902 val out = mk_var(last names,foldr (op-->) (last types) (butlast types))
2223 let val types = map (type_of o lhs o concl) destructors
2224 val encs = map (get_encode_function target) types
2353 let val types = map (type_of o rand o lhs o concl) (CONJUNCTS thm)
2355 INST_TYPE (tryfind_e Empty (C match_type t) types) thm
3386 (* Returns the list of all types in recursion, or nested recursion, *)
4241 let val types = map type_of (fst (strip_forall g))
4244 REWRITE_TAC (map (FULL_ENCODE_DETECT_THM target) types) THEN
4245 REWRITE_TAC (map (FULL_ENCODE_DECODE_THM target) types) THEN