lean2/tests/lean/run/nat_bug4.lean

import logic
open eq.ops

inductive nat : Type :=
zero : nat,
succ : nat → nat
namespace nat
definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
infixl `+`:65 := add
definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
infixl `*`:75 := mul

axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
open eq
theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m
:= subst (mul_succ_right _ _) (eq.refl (n * succ l + m))
end nat
chore(*): minimize dependencies on tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-25 02:58:48 +00:00			`import logic`
refactor(library): rename namespace eq_ops to eq.ops 2014-10-02 00:51:17 +00:00			`open eq.ops`
fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 23:00:38 +00:00
			`inductive nat : Type :=`
feat(*): change inductive datatype syntax Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-22 22:46:10 +00:00			`zero : nat,`
			`succ : nat → nat`
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-04 23:36:06 +00:00			`namespace nat`
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-04 22:03:59 +00:00			`definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y`
fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 23:00:38 +00:00			infixl `+`:65 := add
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-04 22:03:59 +00:00			`definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m`
fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 23:00:38 +00:00			infixl `*`:75 := mul

			`axiom mul_succ_right (n m : nat) : n * succ m = n * m + n`
refactor(library): add 'eq' and 'ne' namespaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-05 01:41:06 +00:00			`open eq`
fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 23:00:38 +00:00			`theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m`
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-04 23:36:06 +00:00			`:= subst (mul_succ_right _ _) (eq.refl (n * succ l + m))`
			`end nat`