paperproof
paperproof copied to clipboard
Paper-Proof
Lean theorem proving interface which feels like pen-and-paper proofs.
Hiya, I'm following the instructions provided by both Mathematics in Lean and Paperproof and it seems to be completely broken at the moment. After adding `require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean"...
The Mathlib `have` tactic does not seem to be supported yet, is that right? The following two code snippets are mathematically equivalent, as far as I'm concerned, and it would...
The `calc` tactic has a slightly distracting Paperproof display which privileges the first line of the calc (printing this explicitly) over the later lines. Term-mode `calc` does not seem to...
Each MVarId is now printed at least twice - once in `goalsBefore` and once in `goalsAfter` (sometimes unnecessary even more from parent nodes when it already handled in the subtree...
Hello, Paperproof looks really interesting :) Do you plan to support other editors besides VS Code like Neovim & Emacs? Thanks
``` theorem pow_dvd_pow_of_dvd {a b : α} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n | 0 => by rw [pow_zero,...
 For example for cases the syntax to the cases tactic is everything with all insides, but we split by `\n` and therefore we display...
Tactic name we have: `coe inv` Tactic name expected: `rwa [coe_inv]`
In the toast below, there should be a button "Add Paperproof import", that automatically adds Paperproof at the top of the file.
We'd quite like types for https://github.com/leanprover/vscode-lean4, but they don't have this package on npm & can't download from github (maybe needs to be done in some other way). Maybe we...
Metadata
Owner
Metadata
Lean theorem proving interface which feels like pen-and-paper proofs.