Lines Matching refs:Type
23 val (ty1, ty2) = Lib.with_exn Type.dom_rng ty err
31 val state_ty = Type.mk_vartype "'state"
37 tm2 |> Term.type_of |> Type.dom_rng |> fst))
40 (Term.inst [Type.alpha |-> ty, Type.beta |-> Term.type_of tm2] tm1,
55 (Term.inst [Type.alpha |-> ty1,
56 Type.beta |-> ty,
68 val get_state_ty = fst o Type.dom_rng o snd o Type.dom_rng o Term.type_of
94 Term.mk_comb (Term.inst [Type.alpha |-> ity, state_ty |-> ty] tm,