Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Re. What is this 3 levels of lambda calculi

view this post on Zulip Email Gateway (Aug 22 2022 at 09:01):

From: "Jens-D. Doll" <jd@cococo.de>
That's a simple and wonderful idea, you asked explanation for. The
problems around this way of structuring are manifold. If you regard a
proof/some software as a tree of sub-proofs you need to verify the
connections, i.e. the types at the vertices. As long as there is no
commonly agreed (and published) type model you can only rely upon
non-typed text substitution. Go ahead; try to define it for 2 or more
levels...

Regards,
Jens

view this post on Zulip Email Gateway (Aug 22 2022 at 09:02):

From: Askar Safin <safinaskar@mail.ru>

Go ahead; try to define it for 2 or more
levels...
I already understand this 2 levels, thanks

==
Askar Safin
http://vk.com/safinaskar
Kazan, Russia

Last updated: Apr 25 2024 at 08:20 UTC