lean2/tests/lean/interactive/t7.lean

Import int.
(** import("tactic.lua") **)
Variable q : Int -> Int -> Bool.
Variable p : Int -> Bool.
Axiom Ax (a b : Int) (H : q a b) : p b.
Variable a : Int.
Theorem T (x : Int) : (q a x) => (p x).
    (** imp_tac() **).
    apply (Ax a).
    exact.
    done.
refactor(builtin): only load the kernel and natural numbers by default Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-30 21:35:37 +00:00			`Import int.`
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-26 23:54:53 +00:00			`( import("tactic.lua") )`
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-06 04:08:36 +00:00			`Variable q : Int -> Int -> Bool.`
			`Variable p : Int -> Bool.`
			`Axiom Ax (a b : Int) (H : q a b) : p b.`
			`Variable a : Int.`
			`Theorem T (x : Int) : (q a x) => (p x).`
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-26 23:54:53 +00:00			`( imp_tac() ).`
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-06 04:08:36 +00:00			`apply (Ax a).`
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-26 23:54:53 +00:00			`exact.`
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-06 04:08:36 +00:00			`done.`