Merge pull request #16 from lean-ja/feature/improve_bintree_functor

lean-ja · Mar 16, 2024 · 740cefe · 740cefe
2 parents f3f67ca + be0be8d
commit 740cefe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/functional-programming-lean/solutions/Solutions/TypeClasses/StandardClasses.lean b/functional-programming-lean/solutions/Solutions/TypeClasses/StandardClasses.lean
@@ -45,6 +45,6 @@ def mapBinTree (f: α → β) : BinTree α → BinTree β
   | BinTree.branch l x r => BinTree.branch (mapBinTree f l) (f x) (mapBinTree f r)
 
 instance : Functor BinTree where
-  map f b := mapBinTree f b
+  map := mapBinTree
 
 #eval  (· + 100) <$> (BinTree.branch (BinTree.branch BinTree.leaf 1 BinTree.leaf) 2 (BinTree.branch BinTree.leaf 3 BinTree.leaf))