acl2/ml/polytypicLib.sml

740 (* base_type       : hol_type -> hol_type                                    *)
796 fun base_type t =
798         handle e => wrapException "base_type" e;
820         fun is_nested t' = not (exists (can (C match_type (base_type t'))) mr_set)
1955         ("The translation " ^ type_to_string (base_type t1) ^ " --> " ^
1961 fun vbase_type t = base_type t handle _ => t
2106 fun add_coding_function target t name function = add_coding_function_precise target (base_type t handle _ => t) name function
2119         exists_coding_theorem_precise target (base_type t handle _ => t) name
2130 fun add_coding_theorem target t name thm = add_coding_theorem_precise target (base_type t handle _ => t) name thm
2212 fun add_source_function t name x = add_source_function_precise (base_type t handle _ => t) name x
2223         exists_source_theorem_precise (base_type t handle _ => t) name
2252 fun add_source_theorem t name thm = add_source_theorem_precise (base_type t handle _ => t) name thm;
2603     val _ = if base_type t = t orelse
2605                then () else (gct target name (base_type t) ; ())
2649         val _ = if base_type t = t orelse
2651                    then () else (gst name (base_type t) ; ())
2822         val base_types = split_nested_recursive_set (base_type t) handle e => wrap "" e
3139                                 (split_nested_recursive_set (base_type t)));
3312         val all_types = flatten (map (op:: o (I ## fst)) (split_nested_recursive_set (base_type t)))
3467                         val _ = map (generate_coding_function target name o base_type) required
3477                         val _ = map (generate_coding_function target name o base_type) required
3487                         val _ = map (generate_source_function name o base_type) required