README.md doesn’t say that it’s a Lean verifier
girving opened this issue · 4 comments
The README is only about the internal implementation (which is cool!), but doesn’t say what the project does. It would be nice to have a few sentence section saying it’s for independently checking Lean proofs.
Touché. I'm going to leave this open for a short time; there's a rewrite in the works to make some big simplifications, get rid of the macros, and remove the integer indirection. I'll overhaul the README when that goes up.
@girving As part of an overhaul to get in all of the Lean 4 changes, the README has been updated to be more descriptive. It also links to a separate book all about type checking and exporting for Lean 4 which covers things in more depth.
Feel free to re-open this or file a separate PR if you have additional input.
Thank you! Though I’ll note that the README for the book on GitHub doesn’t link to the book’s website. :)
Fixed, good eye.