diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index fcebe46f89..6f99102d88 100644 --- a/doc/examples/bintree.lean +++ b/doc/examples/bintree.lean @@ -21,7 +21,7 @@ inductive Tree (β : Type v) where deriving Repr /-| -The function `contains` returns `true` iff the given gree contains the key `k`. +The function `contains` returns `true` iff the given tree contains the key `k`. -/ def Tree.contains (t : Tree β) (k : Nat) : Bool := match t with