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

fix(examples/lean/even): use new name for distribute right theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-07 13:44:53 -08:00
parent 0a20356a51
commit 4523a9f22a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/lean/even.lean
View file

@ -35,7 +35,7 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
exists::intro (w1 + w2) exists::intro (w1 + w2)
(calc a + b = 2*w1 + b : { Hw1 } (calc a + b = 2*w1 + b : { Hw1 }
... = 2*w1 + 2*w2 : { Hw2 } ... = 2*w1 + 2*w2 : { Hw2 }
... = 2*(w1 + w2) : symm (distribute 2 w1 w2)) ... = 2*(w1 + w2) : symm (distributer 2 w1 w2))
-- In the following example, we omit the arguments for add::assoc, refl and distribute. -- In the following example, we omit the arguments for add::assoc, refl and distribute.
-- Lean can infer them automatically. -- Lean can infer them automatically.
@ -56,7 +56,7 @@ theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
(calc a + 1 = 2*w + 1 + 1 : { Hw } (calc a + 1 = 2*w + 1 + 1 : { Hw }
... = 2*w + (1 + 1) : symm (add::assoc _ _ _) ... = 2*w + (1 + 1) : symm (add::assoc _ _ _)
... = 2*w + 2*1 : refl _ ... = 2*w + 2*1 : refl _
... = 2*(w + 1) : symm (distribute _ _ _)) ... = 2*(w + 1) : symm (distributer _ _ _))
-- The following command displays the proof object produced by Lean after -- The following command displays the proof object produced by Lean after
-- expanding macros, and infering implicit/missing arguments. -- expanding macros, and infering implicit/missing arguments.