Let's use Occam razor. Why on earth anybody would be interested in Metamath
> which is even more obscure than Coq or Lean?
>
I just came across a recent presentation by Philip Wadler. The man behind
Haskell and the monads.
https://www.college-de-france.fr/site/xavier-leroy/seminar-2019-12-12-11h15.htm
He doesn't seem to appreciate Coq as a system for teaching logic. Here he
uses Agda to teach simply typed lambda calculus
(terms evaluation, extrinsic and intrinsic typing ...)
The book he is using is:
https://plfa.github.io/
Metamath has a formalization of simply typed lambda calculus by Mario
Carneiro.
http://us.metamath.org/holuni/mmhol.html
You can use Philip Wadler's book to catch what it is all about before
delving into Carneiro's code.
--
FL
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/8693ba68-81e1-40fe-b9f1-78276db75a60%40googlegroups.com.
