Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
Did some more exercises in the Logic section of the Mathematics in Lean book.[1] These introduced proof terms which are just a series of function applications with a more elegant lambda-like syntax. Proof terms underscore that proofs in Lean are really just functions from types to types that compile. As a I side note, the annoyance about having to guess theorem names to solve exercises remains. Hopefully I'll get better at this in the future or find better tools to help. https://github.com/agostbiro/mathematics_in_lean/commit/4aa78ca0f8d8dc4c983b429f5dab26d26b726aa7
0 reply
0 recast
2 reactions
