Lines Matching refs:Type
15 fun mk_word_type ty = fcpSyntax.mk_cart_type (Type.bool, ty)
22 val _ = a = Type.bool orelse
40 (Term.inst [Type.alpha |-> Type.bool, Type.beta |-> dim_of w] fcp_index_tm,
57 (fn tm => fn ty => Term.inst [Type.alpha |-> ty] tm)
69 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty))
142 Term.mk_comb (Term.inst [Type.alpha |-> dim_of w] tm,
158 Term.mk_comb (Term.inst [Type.alpha |-> dim_of a] tm,
168 (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, w))
209 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] tm, w))
225 Term.mk_comb (Term.inst [Type.alpha |-> d, Type.beta |-> ty] tm, l)
316 Term.list_mk_comb (Term.inst [Type.alpha |-> ty] tm, [n, l]))
329 handle HOL_ERR _ => Type.gamma
332 (Term.inst [Type.alpha |-> d1, Type.beta |-> d2,
333 Type.gamma |-> d3] tm, [w1, w2])
348 handle HOL_ERR _ => Type.beta
351 (Term.inst [Type.alpha |-> d1, Type.beta |-> d2] tm, [n, w])
359 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] word_replicate_tm,
388 Term.list_mk_comb (Term.inst [Type.alpha |-> ty] tm, [n1, n2, n3]))
403 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] tm,