2025-04-25.
- still reading JAM paper
- my guess is that the onchain component will become a bottleneck
- also solved the third file of GlimpseOfLean.
- This tutorial introduces BHK-interpretation of the intuitionistic logic.
- Learned
apply?.
- also solved the fourth file
- I pretty much liked the fact that the idiomatic style doesn't introduce any automatically generated names (if such a thing exists in Lean).