From 794088949512c9f76d2dda7ebd23e8636b89f817 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jun 2015 11:29:17 -0700 Subject: [PATCH] fix(doc/lean/library_style): adjust to reflect changes in the standard library --- doc/lean/library_style.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/lean/library_style.org b/doc/lean/library_style.org index 89d8ca4c54..fe3a477ede 100644 --- a/doc/lean/library_style.org +++ b/doc/lean/library_style.org @@ -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