Paper-Proof/paperproof

Issues

• How can I suppress "parseTree XXXms" output?

  #40 opened 3 months ago by minaph
  2

• Mathlib `have` tactic support

  #38 opened 4 months ago by hrmacbeth
  2

• `calc` tactic display

  #39 opened 4 months ago by hrmacbeth
  0

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

  #37 opened 4 months ago by antonkov
  0

• Support other editors

  #36 opened 5 months ago by 9s-l-s9
  1

• lean - theorem from mathlib that doesn't fully work

  #25 opened 8 months ago by lakesare
  2

• Syntax assigned to tactic is incorrect

  #33 opened 6 months ago by antonkov
  0

• lean - rwa tactic name

  #32 opened 6 months ago by lakesare
  1

• Some notes

  #9 opened 6 months ago by lakesare
  2

• Parser.lean - parse tactic combinators

  #12 opened 6 months ago by lakesare
  1

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

  #31 opened 6 months ago by lakesare
  0

• Calc command doesn't work

  #27 opened 8 months ago by antonkov
  1

• lake update failed

  #28 opened 8 months ago by dannypsnl
  2

• Re:window resizing issue, arrow deletion issue

  #11 opened 8 months ago by lakesare
  3

• app - copypasting node contents should be possible

  #22 opened 8 months ago by lakesare
  2

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

  #23 opened 8 months ago by lakesare
  0

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

  #24 opened 10 months ago by lakesare
  0

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

  #21 opened 10 months ago by lakesare
  3

• app - make zooming better

  #14 opened 10 months ago by lakesare
  1

• app - how should focusing work

  #20 opened 10 months ago by lakesare
  1

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

  #15 opened 10 months ago by lakesare
  1

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

  #13 opened 10 months ago by lakesare
  1

• app - add bgs for deeper windows

  #16 opened a year ago by lakesare
  1

• app - fix the lazy-loaded UI

  #19 opened a year ago by lakesare
  1

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

  #18 opened a year ago by antonkov
  2

• extension - we want types from vscode-lean4

  #17 opened a year ago by lakesare
  0

• Why it's important to check whether hypothesis was matched by id already

  #10 opened a year ago by lakesare
  1