Skip to content

Commit

Permalink
Update type_classes.md
Browse files Browse the repository at this point in the history
Make code agree with results
  • Loading branch information
Erotemic committed Oct 1, 2023
1 parent 84e4163 commit 6643a27
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion type_classes.md
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ We can now reimplement `double` using an instance implicit by:
# instance : Add Nat where
# add := Nat.add
# instance : Add Int where
# add := Int.add
# add := Int.mul
# instance : Add Float where
# add := Float.add
def double [Add a] (x : a) : a :=
Expand Down

0 comments on commit 6643a27

Please sign in to comment.