Missing parenthesis in one of the non-computer-checked formulas. (As mentioned in #43.)
succ_inj actually takes a and b as implicit arguments. I guess the entry in the "Theorem statements" in the in-game side bar (where I noticed the error) is generated from the "Axiom" declaration in the code (which I changed).
Aside: I imagine it would be great if the stated types of axioms were checked against the actual types in the corresponding definitions (in src/mynat/definition.lean in this case). See also #39. And note that even in the actual type of e.g. add_zero (as seen in error messages), the name of the variable differs from the type in the documentation side bar: m vs. a.
PS: Wrote my first Lean code today, thanks for the game!
Missing parenthesis in one of the non-computer-checked formulas. (As mentioned in #43.)
succ_injactually takesaandbas implicit arguments. I guess the entry in the "Theorem statements" in the in-game side bar (where I noticed the error) is generated from the "Axiom" declaration in the code (which I changed).Aside: I imagine it would be great if the stated types of axioms were checked against the actual types in the corresponding definitions (in
src/mynat/definition.leanin this case). See also #39. And note that even in the actual type of e.g.add_zero(as seen in error messages), the name of the variable differs from the type in the documentation side bar:mvs.a.PS: Wrote my first Lean code today, thanks for the game!