leanprover/verso

Issues

• Small typo in README

  #98 opened 7 months ago by chenson2018
  1

• Reduce size of generated HTML

  #96 opened 8 months ago by david-christiansen
  0

• Missing \hyperlink in LaTeX

  #71 opened 8 months ago by david-christiansen
  0

• multi-lang support

  #76 opened 9 months ago by Seasawher
  2

• Support for multiline math formulas

  #54 opened 10 months ago by utensil
  5

• Check in CI that there's no `import Lean` checked in

  #82 opened 8 months ago by david-christiansen
  0

• question: can we use verso by simply adding `require verso` to the lakefile?

  #77 opened 9 months ago by Seasawher
  1

• leanOutput Code action removes a `

  #80 opened 9 months ago by nomeata
  0

• Add an example of a minimal genre

  #74 opened 9 months ago by david-christiansen
  0

• Confusing error message with include

  #70 opened 9 months ago by PatrickMassot
  0

• Parser doesn't say "expected" always

  #69 opened 9 months ago by david-christiansen
  0

• Go-to-def for {include A.B.C}

  #68 opened 9 months ago by david-christiansen
  0

• Manual genre: multiple author rendering

  #67 opened 9 months ago by david-christiansen
  0

• toggle displaying information

  #66 opened 10 months ago by Seasawher
  1

• CI: The PDF user's guide is not being placed where expected

  #57 opened 10 months ago by david-christiansen
  0

• Support manually-specified token categories for fragments

  #15 opened a year ago by david-christiansen
  1

• Save Lean example contexts for later

  #42 opened a year ago by david-christiansen
  1

• Have matching begin-end keywords light each other up

  #14 opened a year ago by david-christiansen
  0

• static site generator

  #32 opened a year ago by arademaker
  1

• Unclear how to embed (page-specific) JS

  #37 opened a year ago by Kha
  2

• Bogus highlighting in some recursive functions

  #13 opened a year ago by david-christiansen
  0

• HTML highlighting doesn't show types

  #27 opened a year ago by david-christiansen
  0

• Add a way to include an expression/proof with a given type, where the type doesn't show up in the text

  #10 opened a year ago by david-christiansen
  0

• Add a way to specify scopes (global or local) of expressions

  #9 opened a year ago by david-christiansen
  0

• Generate RSS/Atom feeds

  #16 opened a year ago by david-christiansen
  0

• Generate self-contained HTML

  #12 opened a year ago by david-christiansen
  0

• Newlines do not count as whitespace.

  #11 opened a year ago by nomeata
  1

• PANIC at Lean.PersistentHashMap.find! Lean.Data.PersistentHashMap:160:14: key is not in the map

  #5 opened a year ago by nomeata
  2

• PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none

  #2 opened a year ago by nomeata
  4

• Wrong nesting of <section>

  #6 opened a year ago by nomeata
  0

• Hash-commands not printed in codeblocks?

  #7 opened a year ago by nomeata
  0

• Double-hover

  #8 opened a year ago by nomeata
  1

• #exit not supported

  #3 opened a year ago by nomeata
  2

• lake script generate does not show build errors

  #4 opened a year ago by nomeata
  1