Paper-Proof/paperproof issues and pull requests

#40 - How can I suppress "parseTree XXXms" output?

Issue - State: closed - Opened by minaph 8 months ago - 2 comments

#39 - `calc` tactic display

Issue - State: open - Opened by hrmacbeth 9 months ago

#38 - Mathlib `have` tactic support

Issue - State: open - Opened by hrmacbeth 9 months ago - 2 comments

#37 - Parser can be optimized further by separating pretty-print and tree construction into two different stages

Issue - State: open - Opened by antonkov 10 months ago

#36 - Support other editors

Issue - State: open - Opened by 9s-l-s9 10 months ago - 1 comment
Labels: help wanted

#35 - Fix typos in CONTRIBUTING.md and README.md

Pull Request - State: closed - Opened by pitmonticone 10 months ago - 1 comment

#34 - Dev

Pull Request - State: closed - Opened by lakesare 11 months ago - 1 comment

#33 - Syntax assigned to tactic is incorrect

Issue - State: open - Opened by antonkov 11 months ago

#32 - lean - rwa tactic name

Issue - State: open - Opened by lakesare 12 months ago - 1 comment

#31 - new frontend - we can use vscode right-click menu instead of implementing our own

Issue - State: closed - Opened by lakesare 12 months ago

#30 - Just html

Pull Request - State: closed - Opened by lakesare 12 months ago

#29 - Fix parser to correctly link calc example

Pull Request - State: closed - Opened by antonkov about 1 year ago

#28 - lake update failed

Issue - State: closed - Opened by dannypsnl about 1 year ago - 2 comments

#28 - lake update failed

Issue - State: closed - Opened by dannypsnl about 1 year ago - 2 comments

#27 - Calc command doesn't work

Issue - State: closed - Opened by antonkov about 1 year ago - 1 comment

#26 - Fix typos

Pull Request - State: closed - Opened by pitmonticone about 1 year ago

#26 - Fix typos

Pull Request - State: closed - Opened by pitmonticone about 1 year ago

#26 - Fix typos

Pull Request - State: closed - Opened by pitmonticone about 1 year ago

#26 - Fix typos

Pull Request - State: closed - Opened by pitmonticone about 1 year ago

#25 - lean - theorem from mathlib that doesn't fully work

Issue - State: open - Opened by lakesare about 1 year ago - 2 comments

#24 - app - add a button that will automatically add "import Paperproof" to the top of the file

Issue - State: open - Opened by lakesare about 1 year ago

#24 - app - add a button that will automatically add "import Paperproof" to the top of the file

Issue - State: open - Opened by lakesare about 1 year ago

#24 - app - add a button that will automatically add "import Paperproof" to the top of the file

Issue - State: open - Opened by lakesare about 1 year ago

#23 - lean - how to best let people update/install/remove Paperproof

Issue - State: closed - Opened by lakesare about 1 year ago

#23 - lean - how to best let people update/install/remove Paperproof

Issue - State: closed - Opened by lakesare about 1 year ago

#23 - lean - how to best let people update/install/remove Paperproof

Issue - State: closed - Opened by lakesare about 1 year ago

#22 - app - copypasting node contents should be possible

Issue - State: closed - Opened by lakesare over 1 year ago - 2 comments

#22 - app - copypasting node contents should be possible

Issue - State: closed - Opened by lakesare over 1 year ago - 2 comments

#22 - app - copypasting node contents should be possible

Issue - State: closed - Opened by lakesare over 1 year ago - 2 comments

#21 - extension - add "Pls do `import PaperProof`" error in the extension

Issue - State: closed - Opened by lakesare over 1 year ago - 3 comments

#21 - extension - add "Pls do `import PaperProof`" error in the extension

Issue - State: closed - Opened by lakesare over 1 year ago - 3 comments

#21 - extension - add "Pls do `import PaperProof`" error in the extension

Issue - State: closed - Opened by lakesare over 1 year ago - 3 comments

#20 - app - how should focusing work

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#19 - app - fix the lazy-loaded UI

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#19 - app - fix the lazy-loaded UI

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#19 - app - fix the lazy-loaded UI

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#18 - Info at cursor bet Lean processes file is dropped and not sent to server/webview

Issue - State: closed - Opened by antonkov over 1 year ago - 2 comments

#18 - Info at cursor bet Lean processes file is dropped and not sent to server/webview

Issue - State: closed - Opened by antonkov over 1 year ago - 2 comments

#18 - Info at cursor bet Lean processes file is dropped and not sent to server/webview

Issue - State: closed - Opened by antonkov over 1 year ago - 2 comments

#17 - extension - we want types from vscode-lean4

Issue - State: open - Opened by lakesare over 1 year ago

#17 - extension - we want types from vscode-lean4

Issue - State: open - Opened by lakesare over 1 year ago

#17 - extension - we want types from vscode-lean4

Issue - State: open - Opened by lakesare over 1 year ago

#16 - app - add bgs for deeper windows

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#16 - app - add bgs for deeper windows

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#15 - Parser.lean - make `theorem smth : smth := by` work

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#15 - Parser.lean - make `theorem smth : smth := by` work

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#15 - Parser.lean - make `theorem smth : smth := by` work

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#14 - app - make zooming better

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#14 - app - make zooming better

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#13 - Parser.lean - return `isError` if there is one in the `InfoTree` (if possible)

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#12 - Parser.lean - parse tactic combinators

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#12 - Parser.lean - parse tactic combinators

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#11 - Re:window resizing issue, arrow deletion issue

Issue - State: closed - Opened by lakesare over 1 year ago - 3 comments

#11 - Re:window resizing issue, arrow deletion issue

Issue - State: closed - Opened by lakesare over 1 year ago - 3 comments

#10 - Why it's important to check whether hypothesis was matched by id already

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#10 - Why it's important to check whether hypothesis was matched by id already

Issue - State: closed - Opened by lakesare over 1 year ago - 1 comment

#9 - Some notes

Issue - State: closed - Opened by lakesare over 1 year ago - 2 comments

#9 - Some notes

Issue - State: closed - Opened by lakesare over 1 year ago - 2 comments

#8 - New parser

Pull Request - State: closed - Opened by antonkov over 1 year ago

#8 - New parser

Pull Request - State: closed - Opened by antonkov over 1 year ago

#7 - Migrate to tldraw v2

Pull Request - State: closed - Opened by antonkov over 1 year ago

#7 - Migrate to tldraw v2

Pull Request - State: closed - Opened by antonkov over 1 year ago

#6 - New parser

Pull Request - State: closed - Opened by antonkov over 1 year ago

#6 - New parser

Pull Request - State: closed - Opened by antonkov over 1 year ago

#5 - Remove duplicate line from README

Pull Request - State: closed - Opened by ddrone over 1 year ago - 1 comment

#5 - Remove duplicate line from README

Pull Request - State: closed - Opened by ddrone over 1 year ago - 1 comment

#4 - Made it so that if you work in the browser you only need to run 1 thing insead of 2 things

Pull Request - State: closed - Opened by lakesare over 1 year ago

#4 - Made it so that if you work in the browser you only need to run 1 thing insead of 2 things

Pull Request - State: closed - Opened by lakesare over 1 year ago

#3 - WIP: Everything together 2

Pull Request - State: closed - Opened by lakesare over 1 year ago - 2 comments

#3 - WIP: Everything together 2

Pull Request - State: closed - Opened by lakesare over 1 year ago - 2 comments

#2 - WIP: Everything together

Pull Request - State: closed - Opened by lakesare over 1 year ago

#2 - WIP: Everything together

Pull Request - State: closed - Opened by lakesare over 1 year ago

#1 - Add some documentation about getting started in README.md

Pull Request - State: closed - Opened by ddrone over 1 year ago

GitHub / Paper-Proof/paperproof issues and pull requests