From 9c72917f5ecc0b92beb8e525784069cfa5eecff2 Mon Sep 17 00:00:00 2001 From: William Blake <35980963+langfield@users.noreply.github.com> Date: Mon, 9 May 2022 03:44:48 -0400 Subject: [PATCH] doc: fix typo gree -> tree --- doc/examples/bintree.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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