Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?

>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
Kazan, Russia

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.