[isabelle-dev] handle TYPE _

Makarius makarius at sketis.net
Wed Sep 15 18:23:20 CEST 2010

On Wed, 15 Sep 2010, Walther Neuper wrote:

> Now a simple question, which might be caused by my missing experience of 
> how to handle Toplevel errors:
> I want to adapt code which tries to check types somehow as follows:
> ML {*
> Toplevel.debug := true;
> cterm_of @{theory} (@{term "a"} $ @{term "b"})
> handle TYPE _ => writeln "type error found";
> *}
> This results in the response buffer with:
> *** val it = () : unit
> *** Error (line 3):
> *** Can't unify cterm to {} (Incompatible types)
> *** Exception- ERROR "Static Errors" raised
> *** At command "ML".
> How are such type checks done nowadays ?

This is really just a plain type error: writeln produces (): unit, but the 
invocation of cterm_of a cterm.

> PS: I know that ctxt's are to be preferred to thy's; this will be done 
> in the next step of re-engineering.

cterm_of/ctyp_of is one of the very few points where a theory certificate 
appears in regular user-space code.  The typically you pass on 
certifiedness from one entity to another newly produced one.  Often the 
theory in question is obtain via Thm.theory_of_thm or Thm.theory_of_cterm.


More information about the isabelle-dev mailing list