Re: [isabelle] typecheck a term
One way is to call the function cterm_of, which converts a raw term
to a "certified term". Note that typechecking only makes sense in the
context of a theory. The most basic theory is ProtoPure.thy, which
only knows about the meta-logic connectives. Or HOL.thy (for the
basic HOL types) or Main.thy (for everything).
On 23 Feb 2006, at 04:14, Sean McLaughlin wrote:
I needed to create some Isabelle terms by hand, and would like to
sure they typecheck as a sanity check. So, eg.
Const ("==", "bool => bool => bool") $ Free ("a", "bool") $
Free ("b", "prop") : Term.term
Doesn't typecheck. What function do I call?
This archive was generated by a fusion of
Pipermail (Mailman edition) and