lean2/tests/lean/run/tactic17.lean

import logic
open tactic

constant A : Type.{1}
constant f : A → A → A

theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
:= by apply (@congr A A _ _ (f a) (f b));
      apply (congr_arg f);
      !assumption
chore(*): minimize dependencies on tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-24 19:58:48 -07:00			`import logic`
feat(frontends/lean): rename 'using' command to 'open' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-09-03 16:00:38 -07:00			`open tactic`
fix(library/unifier): missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-03 10:50:08 -07:00
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-10-02 16:20:52 -07:00			`constant A : Type.{1}`
			`constant f : A → A → A`
fix(library/unifier): missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-03 10:50:08 -07:00
			`theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c`
refactor(library/logic): remove 'core' subdirectory 2014-10-05 10:50:13 -07:00			`:= by apply (@congr A A _ _ (f a) (f b));`
fix(lean/library/standard): fix tests, more cleanup 2014-08-20 15:49:44 -07:00			`apply (congr_arg f);`
fix(library/unifier): missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-03 10:50:08 -07:00			`!assumption`