Lines Matching defs:ty
16 fun Undef ty =
17 raise Fail ("Undef: "^Lib.quote (Parse.type_to_string ty)^
39 fun unc c = let val (cname,ty) = dest_const c
40 val (dtys,rty) = boolSyntax.strip_fun ty
41 val ty' = if null dtys then rty else
43 in mk_var(cname,ty')
49 val ty = snd(strip_fun(type_of (hd Clist)))
50 val args = snd(dest_type ty)
53 val flist_types = map (fn ty => (ty --> termty)) args
56 val lift_type = list_mk_fun(flist_types@[ty],termty)
98 add_string ("fun lift_"^ #2 tyop^" ty = "),
106 add_string " = map (TypeBasePure.cinst ty) Clist",