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.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
