[isabelle-dev] exception TERM raised (line 141 of "Syntax/syntax_trans.ML"): abs_tr
makarius at sketis.net
Sat Nov 5 10:45:53 CET 2011
On Fri, 4 Nov 2011, Brian Huffman wrote:
> Better yet, the "syntax" command probably ought to be used only with
> types containing nothing but nonterminals:
> syntax "_lebesgue_integral" :: "pttrn => logic => logic => logic"
> ("\<integral> _. _ \<partial>_" [60,61] 110)
> Using any other kind of type expression with a "syntax" command is
> essentially a comment; such types are only used for generating
> nonterminals (type variables go to "any", type prop goes to "prop",
> other logical types go to "logic") and are not used for typechecking.
Such a non-conservative change always needs 2-3 good reasons for it and
almost nothing against it -- to justify the effort required to get the
implementation right and adapt existing applications.
I agree that "comments" are often deceptive, but the traditional idiom for
Isabelle syntax uses the types exactly as such, to illustrate a little bit
the intention of the notation. (I have maintained all reachable syntax
declarations for many years.) See e.g.
for an arbitrary example. Even for a proper term constant the type scheme
is just an approximation for the intended meaning. For syntax the
syntactic type does the same, although the type system happens to be
Furthermore, asking users to write actual nonterminals exposes more
technical details than necessary. I never know myself on the spot where
to put "logic" or "any" (it also depends on the LHS or RHS), and there are
also "prop" vs. "prop'", for example. I do know the system does it right
when a certain standard idiom is followed. (This is also what I did for
5c760e1692b3, and used the "pttrn" stemming from existing practice,
without delving into old questions about "pttrn" vs. "idt" again.)
More information about the isabelle-dev