Post #2236922
2026-05-02 19:28 UTC
@jonmsterling@mathstodon.xyz At the very least, even the current Isabelle would benefit from using more Scheme/Racket-inspired quotation mechanisms like Lean.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-02 19:31
@zwarich@hachyderm.io Yeah, absolutely. Well, to be honest, I think Lean might be the right ML in which to build the next LCF.