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).

Larry


On 23 Feb 2006, at 04:14, Sean McLaughlin wrote:

I needed to create some Isabelle terms by hand, and would like to make
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 MHonArc.