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

fix(examples/lean): comments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-06 11:48:27 -08:00
parent 62bb2ab2f9
commit 8029134758
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

@ -37,10 +37,10 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
... = 2*w1 + 2*w2 : { Hw2 } ... = 2*w1 + 2*w2 : { Hw2 }
... = 2*(w1 + w2) : symm (distribute 2 w1 w2)) ... = 2*(w1 + w2) : symm (distribute 2 w1 w2))
-- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::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.
-- --
-- Refl is the reflexivity proof. (Refl a) is a proof that two -- refl is the reflexivity proof. (refl a) is a proof that two
-- definitionally equal terms are indeed equal. -- definitionally equal terms are indeed equal.
-- "definitionally equal" means that they have the same normal form. -- "definitionally equal" means that they have the same normal form.
-- We can also view it as "Proof by computation". -- We can also view it as "Proof by computation".