[isabelle-dev] Error with case syntax?
makarius at sketis.net
Sat Jun 1 14:42:06 CEST 2013
On Fri, 31 May 2013, Jasmin Christian Blanchette wrote:
> Hi all,
> Using Isabelle/c3f837d92537,
> theory Bug imports Main begin
> lemma "(case p of (a, b) => f (a, b)) = f p"
> *** exception TERM raised (line 332 of "term.ML"): fastype_of: expected function type
> in Proof General and in "isabelle tty" but not in jEdit.
The error did not show up in in Isabelle/jEdit, because the (still crude)
mechanism to print proof states asynchronously just failed without further
notice. (Hopefully I will managed this summer to get this all on a more
solid foundation as "asynchronous agents framework" -- when I am back from
my vacation in June.)
Sneaking the exception_trace combinator into Goal_Display.pretty_goals
Exception trace for exception - TERM raised in term.ML line 332
It means that the new case translation uncheck phase by Dmitriy chokes on
an ill-typed term.
The reason for the malformed term is the new Type_Annotation markup that I
had put in the wrong spot -- after having explained to you privately that
it has to be after "uncheck" and before "unparse" (it is relevant for
Sledgehammer Isar output with type annotations). This problem is now
addressed in b12f2cef3ee5.
Moreover, I've made Dmitriy's uncheck function *permissive* in
da42b500a6aa, similar to contraction of term abbreviations. Thus it might
have taken longer to find out about this lapse mine, but print functions
need to be as total as feasibile, to allow certain error situations to be
reported to the user, even if they contain malformed terms.
More information about the isabelle-dev