Issues

• Make epsilon-automation configurable

  PatrickMassot/verbose-lean4#38 · Filter by author pimotte opened on Jun 29, 2026

• Language for more flexible induction

  PatrickMassot/verbose-lean4#36 · Filter by author pimotte opened on Jun 11, 2026

• NameLess Proofs

  PatrickMassot/verbose-lean4#35 · Filter by author pimotte opened on Jun 9, 2026
  2

• Memory use: Upgrading to the module system

  PatrickMassot/verbose-lean4#33 · Filter by author pimotte opened on May 11, 2026
  1

• Language proposal: ... holds for propositional logic

  PatrickMassot/verbose-lean4#23 · Filter by author pimotte opened on Mar 3, 2026
  2

• Update to recent version

  PatrickMassot/verbose-lean4#22 · Filter by author pimotte opened on Mar 3, 2026
  3

• Coincidence between keywords and identifiers

  PatrickMassot/verbose-lean4#12 · Filter by author miguelmarco opened on Feb 10, 2025
  7

• Make a release

  PatrickMassot/verbose-lean4#9 · Filter by author jnarboux opened on Dec 26, 2024
  1

  

• 'We conclude' sometimes too powerful ?

  PatrickMassot/verbose-lean4#5 · Filter by author jnarboux opened on Mar 20, 2024
  1

• misleading error message about linarith

  PatrickMassot/verbose-lean4#4 · Filter by author jnarboux opened on Mar 20, 2024
  1

• Replace turnstyle ⊢ by something more student friendly

  PatrickMassot/verbose-lean4#3 · Filter by author jnarboux opened on Mar 20, 2024