search

clarkgrubb / hyperpolyglot

hyperpolyglot.org
Other
473 stars 94 forks source link

Add Lean4 Theorem prover syntax #131

Open universemaster opened 1 year ago

universemaster commented 1 year ago

A table based format for commands sorted by purpose seems a good fit for Lean 4's theorem prover syntax.

Resources: https://djvelleman.github.io/HTPIwL/ and https://leanprover-community.github.io/

martin12333 commented 10 months ago

where would you want to insert the column for Lean?

my suggestion: https://docs.google.com/spreadsheets/d/1Or_sAxcf8G5VGoIXXEJl8Agaz5FOx6qMwwOy9aFH-e4/edit?usp=sharing (https://docs.google.com/spreadsheets/d/1w4MAxWcWjX3aMBRkOsqjwcAabFtY4WT4JloPRd944og/edit?usp=sharing)

related: a free book on using Lean 4 as a programming language