Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
On Tue, 3 Mar 2015, Larry Paulson wrote:
I think your clue here is the phrase "type-theoretic parlanceâ, which is
to say that people from that background may want to see ==> as a
function type, for example, analogously to LF, which can be regarded as
the type-theoretic analogue of Isabelle Pure.
Yes, this text in the "isar-ref" manual (section 2.1) and a slightly
longer version in the "implementation" manual (chapter 2) emerged from
what I've learned from people in Edinburgh, Cambridge, Nijmegen, and
especially Stefan Berghofer in Munich around 2000. It is an attempt to
explain things in a way that everybody understands, both
strongly-dependent types and classic logicians.
On 3 Mar 2015, at 12:48, Askar Safin <safinaskar at mail.ru> wrote:
The document is isar-ref from isabelle 2013.
By the default, you should use the current official release for
everything, including the continously growing/updated manuals. Presently
it is Isabelle2014 (August 2014).
Also, FAQ doesn't say about levels of lambda calculi.
Before Larry mentioned that, I hardly remembered this ancient relic at
all. Apart from the isabelle-users mailing list, the current Q&A platform
is Stackoverflow: http://stackoverflow.com/questions/tagged/isabelle
You should quickly get some idea who is active where, and which kind of
discussions or question/answer threads are better place on this site or
This archive was generated by a fusion of
Pipermail (Mailman edition) and