Open RoboticMind opened 1 year ago
Think the * needs to be escaped here on this line since it's missing inside of the brakets
and * as a notation for op in a multiplicative monoid, such as ⟨nat, , 1⟩.
Looks like there's a typo on this line:
In practce, Lean provides mechanisms for writing one definition and then cloning it automatically to produce the code for the other.
The solution is already given for the exercise on the notes here. I think that was a mistake?
Might be good to copy paste the source code definition if this is going to be left in. The actually types themselves are just Type u -> Type u
Type u -> Type u
chapter 5
Think the * needs to be escaped here on this line since it's missing inside of the brakets
and * as a notation for op in a multiplicative monoid, such as ⟨nat, , 1⟩.Looks like there's a typo on this line:
5.3.6. Example: default typeclass
The solution is already given for the exercise on the notes here. I think that was a mistake?
5.3.8. Typeclass inheritance
Might be good to copy paste the source code definition if this is going to be left in. The actually types themselves are just
Type u -> Type u