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

fix(library/init/data/array/basic): typo

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-12 09:03:20 -07:00
parent d7de85e1e7
commit 52b72c85bf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/array/basic.lean
View file

@ -110,7 +110,7 @@ def pop (a : Array α) : Array α :=
-- TODO(Leo): justify termination using wf-rec
partial def shrink : Array α → Nat → Array α
| a n := if a.size ≥ n then a else shrink a.pop n
| a n := if n ≥ a.size then a else shrink a.pop n
section
variables {m : Type v → Type v} [Monad m]