leanprover-community/NNG4

Issues

• The commentary uses `repeat` which isn't listed in the tactics

  #60 opened 3 months ago by jariji
  2

• "takes longer"

  #58 opened 3 months ago by jariji
  1

• at h

  #59 opened 3 months ago by jariji
  1

• typo

  #57 opened 3 months ago by jariji
  1

• `at` introduced without explanation

  #45 opened 3 months ago by sullyj3
  2

• There are bugs in generated pot file.

  #56 opened 3 months ago by JiechengZhao
  1

• `simp_add` not available in final boss world

  #54 opened 3 months ago by kbuzzard
  1

• disappearing text in tutorial world entry page

  #26 opened 9 months ago by kbuzzard
  2

• add definitions for Ne and LE.

  #38 opened 3 months ago by joneugster
  1

• `rw`: wrong error message

  #25 opened 9 months ago by joneugster
  1

• Add link to FLT resources

  #22 opened 9 months ago by kbuzzard
  0

• Documentation for tactics and definitions missing

  #11 opened 3 months ago by b-reinke
  2

• Even/odd world

  #9 opened a year ago by kbuzzard
  2

• Strong induction world

  #10 opened a year ago by kbuzzard
  0

• You have not unlocked the tactic 'generalizing' yet!

  #51 opened 3 months ago by mfornet
  2

• Unable to use induction

  #53 opened 4 months ago by mynameismon
  1

• Disable `succ_inj` at Algorithm World 5

  #50 opened 4 months ago by evrimoztamur
  1

• Missing generalizing tactic in AdvMul

  #48 opened 5 months ago by ndren
  1

• Don't allow new users to jump directly to level 1

  #23 opened 7 months ago by kbuzzard
  2

• Devcontainer Setup on MacOS broken

  #35 opened 7 months ago by joneugster
  1

• Pow.pow doesn't render infix

  #46 opened 7 months ago by danielzgtg
  1

• Algorithm World level 6: incorrect theorem statement

  #37 opened 8 months ago by nvchhawch
  0

• No introduction of "backwards rewrite"

  #28 opened 8 months ago by Madjosz
  4

• Rewrite at hypothesis does not work

  #36 opened 8 months ago by mthom
  1

• Implication World level 9 - unable to use `zero_ne_succ` on regular rules

  #31 opened 8 months ago by nvchhawch
  2

• Typo in Implication World level 6

  #30 opened 8 months ago by nvchhawch
  1

• Rip out Proposition world

  #8 opened 9 months ago by kbuzzard
  1

• Let `rfl` close iffs as well as equalities

  #18 opened 9 months ago by kmill
  2

• able to use `zero_mul` to prove itself

  #27 opened 9 months ago by haifron
  1

• Add copyright notices to all files

  #24 opened 9 months ago by kbuzzard
  0

• Can't remove `TacticDoc` linter warning

  #21 opened 9 months ago by kbuzzard
  0

• Playing the game in VsCode

  #19 opened 10 months ago by RexWzh
  1

• Ring tactic

  #12 opened 10 months ago by ifarabella
  4

• horrible typo in current web version

  #14 opened 10 months ago by kbuzzard
  2

• I hate `Level_n.lean`

  #13 opened a year ago by kbuzzard
  6

• easy tactics needed

  #16 opened a year ago by kbuzzard
  3

• Question: How do you run lean4 on mdbook?

  #7 opened a year ago by Seasawher
  3

• How to build locally?

  #5 opened a year ago by Seasawher
  29

• Failed to load resource: net::ERR_CONTENT_LENGTH_MISMATCH

  #4 opened a year ago by jameshfisher
  3