Re: [isabelle] Syntax issue: lost between HOL and Isar
On 8/2/2012 10:42 AM, Lars Noschinski wrote:
"HOL syntax" is not a very useful term here. In Isabelle/Isar, we
distinguish between outer and inner syntax. The inner syntax is the
syntax used to input terms (and types). Apart from trivial cases,
inner syntax needs to be quoted.
The outer syntax is everything else. Most of it is already part of
Pure (i.e. independent of any logic), mainly everything which makes up
proof and document structure; but logics often add additional commands
for logic-specific operations (e.g. "fun" and "inductive" for HOL).
I think I have it.
HOL imports pure, therefore it inherits the Isar language and a default
set of Isar outer syntax commands, where new outer syntax can be defined
with "Outer_syntax.command". Everything in a .thy file is Isar syntax
and everything is HOL syntax, so there's no need to talk about HOL
syntax, since, again, everything is HOL syntax. We could, however,
compare Isabelle/HOL syntax with Isabelle/FOL syntax, where they would
both share the default Isar outer syntax commands.
The word "term" doesn't have a lot of significance to me. I assume you
mean "lambda calculus term", but I see very little lambda calculus in
expressions between double quotes, so it doesn't completely help me to
know what to put in double quotes.
However, it is useful to know that if I see something in double quotes,
I know it must be either a type or a lambda calculus term, even if the
lambda calculus doesn't look like lambda calculus.
This archive was generated by a fusion of
Pipermail (Mailman edition) and