From b887a2b90089f6a3bb3d851afc0d7210a326266d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Dec 2013 08:58:06 -0800 Subject: [PATCH] fix(examples/lean/tactic_in_lua): try to make sure the example works when using LuaJIT Signed-off-by: Leonardo de Moura --- examples/lean/tactic_in_lua.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean index c18daf11d..76e542afb 100644 --- a/examples/lean/tactic_in_lua.lean +++ b/examples/lean/tactic_in_lua.lean @@ -65,7 +65,7 @@ **) Theorem T (a b : Bool) : a => b => a /\ b := _. - apply (** REPEAT(ORELSE(imp_tac, conj_in_lua)) .. assumption_tac **) + apply (** THEN(REPEAT(ORELSE(imp_tac, conj_in_lua)), assumption_tac) **) done (* Show proof created using our script *)