Lines Matching defs:ty
21 (fn (a,(ars,d)) => let val (n,ty) = dest_var a in
23 SOME ty' => if ty = ty' then (a::ars,d) else
24 let val vs = Redblackmap.foldl (fn (n,ty,ls) => mk_var(n,ty)::ls) [] d
26 in (a'::ars,Redblackmap.insert(d,fst(dest_var a'),ty)) end
27 | NONE => (a::ars,Redblackmap.insert(d,n,ty)) end)
35 val (n,ty) = dest_var v
36 val v' = mk_var (Lib.prime n, ty)
40 val nchotomys = map (fn ty => SPEC_ALL (TypeBase.nchotomy_of ty)) tys
45 val count_ty_aux_vars = map (fn (ty,count_name_aux) =>
47 foldr (fn (h,ty) => type_of h --> ty) (ty --> num) helpers))
53 val ty = foldr (fn (x,t) => (x --> num) --> t) (t --> num) ars
54 val ctr = mk_const("count_"^n^"_aux",ty)
78 val (n,ty) = dest_var v
79 val ctr = counter ty
88 (fn (ty,(all,ths)) => let
89 val (th,all) = Lib.pluck (fn th => ty = type_of(fst(dest_forall(concl th)))) all