hhu-adam/Robo

Issues

• Cannot start Primzahlen 8 because of Lean error (ambiguity due to name clash)

  #60 opened a month ago by sozysozbot
  2

• Level 1 crashes when using the recommended `tauto` tactic

  #59 opened a month ago by DanielFabian
  2

• Robo can't find definitions of tactics or theorems

  #57 opened 4 months ago by tautastic
  1

• The Web App runs into runtime exceptions constantly

  #56 opened 4 months ago by tautastic
  5

• Meta-issue: Revision of FunctionSurj

  #55 opened 4 months ago by TentativeConvert
  0

• FunctionSurj, Level 1: Type of f is not displayed.

  #54 opened 4 months ago by TentativeConvert
  3

• Add outro page with summary to each planet.

  #53 opened 4 months ago by TentativeConvert
  0

• "World" at the top of each page should read "Planet" in this game!

  #47 opened 4 months ago by TentativeConvert
  2

• Cantor, level 9: Cantor says „Gute Wahl“ also for incorrect choices

  #51 opened 5 months ago by TentativeConvert
  0

• Categorize tactics according to applicability

  #52 opened 4 months ago by TentativeConvert
  0

• introduce 'trans' on Logos or Implis (and also use it elsewhere)

  #50 opened 5 months ago by TentativeConvert
  2

• documentation of `constructor` tactic should mention iff statements

  #41 opened 5 months ago by TentativeConvert
  1

• MatrixTrace, Level 8: make variable names dynamic

  #42 opened 5 months ago by TentativeConvert
  1

• MatrixTrace, Level 9: Hint needs to mention `trans` explicitly.

  #44 opened 5 months ago by TentativeConvert
  1

• MatrixTrace, Level 9: everyone gets stuck

  #43 opened 5 months ago by TentativeConvert
  1

• MatrixTrace: Can we typeset some matrices in earlier levels to improve readability?

  #48 opened 5 months ago by TentativeConvert
  1

• A sum notation with coercion baked into it

  #49 opened 5 months ago by sinhp
  0

• typo

  #45 opened 5 months ago by TentativeConvert
  0

• Cantor: numbering of files/levels got mixed up

  #46 opened 5 months ago by TentativeConvert
  0

• nth_rw seems to missing from the inventory

  #40 opened 5 months ago by TentativeConvert
  0

• Robotswana 1: unfold stdBasisMatrix kills hints

  #39 opened 6 months ago by TentativeConvert
  1

• Potenzmenge lacks the theorem `Set.union_comm`

  #37 opened 6 months ago by bernborgess
  1

• Remove parentheses from `apply (h.mp) at …` when it becomes possible

  #10 opened 6 months ago by TentativeConvert
  1

• Sum/Babylon: induction without named hypothesis?

  #25 opened 6 months ago by TentativeConvert
  0

• Robotswana 9: hints not displayed because of unfold

  #36 opened 6 months ago by TentativeConvert
  2

• Implis 13: add `imp_iff_not_or` to Inventory

  #28 opened 6 months ago by TentativeConvert
  2

• Robotswana 9: rename variable, align hint with proof

  #35 opened 6 months ago by TentativeConvert
  0

• Robotswana 2, 3: lemmas appear in inventory before the level is completed

  #34 opened 6 months ago by TentativeConvert
  0

• Babylon Level 4 Latex-summary mismatch

  #32 opened 6 months ago by bernborgess
  1

• Function L22_Inverse: explanation of `choose_spec` needs to be included in all branches

  #30 opened 6 months ago by TentativeConvert
  1

• Babylon/04: incorrect latex summary

  #29 opened 6 months ago by TentativeConvert
  1

• Babylon levels 05 & 06: missing latex-summary of exercise

  #27 opened 6 months ago by TentativeConvert
  0

• `by_contra` ignores `tactic.hygienic`

  #26 opened 6 months ago by joneugster
  1

• modify `ring`

  #2 opened 7 months ago by joneugster
  0

• Nat.succ not explained in Luna, level 1

  #23 opened 7 months ago by TentativeConvert
  0

• Predicate/Quantus, Level 10: add additional warning about branch not yet covered

  #24 opened 7 months ago by TentativeConvert
  1

• Wie erklärt man Typ versus Mengen?

  #5 opened a year ago by TentativeConvert
  1

• Implis, Level 13: explain why 'by_cases a : A' does not work

  #20 opened 7 months ago by TentativeConvert
  3

• Remove pipes `<|` from any Statements and hints.

  #18 opened 7 months ago by joneugster
  0

• Logo, Level 14: Third column of table easily becomes invisible.

  #22 opened 7 months ago by TentativeConvert
  1

• 'constructor assumption' produces undefined state

  #21 opened 7 months ago by TentativeConvert
  1

• Quantus, Level 6: explain why 'use n^2/2' does not work

  #19 opened 7 months ago by TentativeConvert
  0

• Level: introduce `congr`

  #17 opened 7 months ago by joneugster
  0

• fix: improve hint in drinkers paradox

  #11 opened 7 months ago by joneugster
  0

• Robo game (still) broken on the server

  #9 opened a year ago by TentativeConvert
  0

• Inequality 3 crashes

  #7 opened a year ago by globin
  2

• Term Modus and forward reasoning

  #1 opened 2 years ago by joneugster
  1

• ext-Strategie für abstrakte Mengen

  #6 opened a year ago by TentativeConvert
  0