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.
http://isabelle.in.tum.de/repos/isabelle/file/5c760e1692b3/src/HOL/Isar_Examples/Hoare.thy#l191
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
slightly different.
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.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
