Re: [isabelle] Syntax issue: lost between HOL and Isar
I've been totally focused on the frontend languages, ML, Isar, and HOL,
while knowing nothing about what the backend prover does with them.
I now have a way to make sense of it all being Isar syntax, the HOL
syntax being a part of the Isar syntax, and HOL not being dependent on Isar.
It could be that Isar is a framework that HOL uses to state lambda
calculus terms, and the backend strips away all the outer syntax, where
all that's left is the HOL lambda calculus terms. That idea lines up
with Christian saying that proofs are irrelevant.
Now I sit on the two ideas and wait to see if I read something that
supports one of the two ideas, that HOL inherits Isar and makes it its
own, or Isar is a framework that gets stripped away by the backend.
Today, right now, I'm leaning towards the idea that much of the Isar
gets stripped away.
(I do see "framework" in "Chapter 2 The Isabelle/Isar Framework", which
is where I must have gotten "framework". I don't see "stripped away"
anywhere yet. There's a lot I haven't read yet.)
I don't really care to know the details of what the backend does, it
would take years to learn about it, but it's nice to make sense of
important high-level concepts.
This archive was generated by a fusion of
Pipermail (Mailman edition) and