michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(doc/lean/library_style): adjust to reflect changes in the standard library

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-16 11:29:17 -07:00
parent 9249ebdaab
commit 7940889495
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/lean/library_style.org
View file

@ -256,7 +256,7 @@ nat.induction_on n
succ (n + m) = succ n + m : symm (succ_add n m)
... = succ n + k : H
... = succ (n + k) : succ_add n k,
have H3 : n + m = n + k, from succ_inj H2,
have H3 : n + m = n + k, from succ.inj H2,
IH H3)
#+END_SRC lean