lean2/tests/lean/tactic3.lean

Variables p q r : Bool

Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
    apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
    done

(* Display proof term generated by previous tactic *)
Show Environment 1
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-29 06:11:07 +00:00			`Variables p q r : Bool`

			`Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.`
feat(frontends/lean/parser): add support for Lua expression code blocks In expression code blocks, we do not have to write a "return". After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write apply ( REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) ) instead of apply ( return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) ) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-29 18:21:17 +00:00			`apply ( REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) )`
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-29 06:11:07 +00:00			`done`

			`(* Display proof term generated by previous tactic *)`
			`Show Environment 1`