max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix typo gree -> tree

Browse source
This commit is contained in:
William Blake 2022-05-09 03:44:48 -04:00 • committed by GitHub
parent 3cd46888bf
commit 9c72917f5e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/examples/bintree.lean
View file

@ -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