*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?*From*: Askar Safin <safinaskar at mail.ru>*Date*: Tue, 03 Mar 2015 15:48:08 +0300*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <44F578A1-F168-49FF-B12C-8C5C395DAA31@cam.ac.uk>*References*: <1425331630.593971199@f411.i.mail.ru> <44F578A1-F168-49FF-B12C-8C5C395DAA31@cam.ac.uk>*Reply-to*: Askar Safin <safinaskar at mail.ru>

>Note that I am moving your question to the Isabelle Usersâ mailing list. > >It would be helpful if you would say which document refers to 3 levels of lambda calculus. Thanks for answer. The document is isar-ref from isabelle 2013. Exact text is "The Pure logic [38, 39] is an intuitionistic fragment of higher-order logic[13]. In type-theoretic parlance, there are three levels of Î-calculus with corresponding arrows =>/\<And>/==>". Also, FAQ doesn't say about levels of lambda calculi. == Askar Safin http://vk.com/safinaskar Kazan, Russia

**Follow-Ups**:**Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?***From:*Larry Paulson

**References**:**Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?***From:*Larry Paulson

- Previous by Date: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Next by Date: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Previous by Thread: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Next by Thread: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list