michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/builtin_tactics): adjust tactics precedence

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-20 17:10:16 -07:00
parent 9b8f60b739
commit e68007a727
4 changed files with 11 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/tools/tactic.lean
View file

@ -39,15 +39,10 @@ opaque definition beta : tactic := builtin
opaque definition unfold {B : Type} (b : B) : tactic := builtin
opaque definition exact {B : Type} (b : B) : tactic := builtin
opaque definition trace (s : string) : tactic := builtin
precedence `;`:200
infixl ; := and_then
-- [ t_1 | ... | t_n ] notation
notation `[` h:100 `|` r:(foldl 100 `|` (e r, or_else r e) h) `]` := r
-- [ t_1 || ... || t_n ] notation
notation `[` h:100 `||` r:(foldl 100 `||` (e r, par r e) h) `]` := r
infixl `;`:15 := and_then
notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r
definition try (t : tactic) : tactic := [t | id]
notation `?` t:max := try t
definition repeat1 (t : tactic) : tactic := t ; !t
definition repeat1 (t : tactic) : tactic := t ; repeat t
definition focus (t : tactic) : tactic := focus_at t 0
definition determ (t : tactic) : tactic := at_most t 1

4
src/frontends/lean/builtin_tactics.cpp
View file

@ -10,13 +10,15 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/parse_table.h"
#define LEAN_APPLY_RBP 16 // it should be bigger than `;` (and_then) precedence
namespace lean {
using notation::transition;
using notation::mk_ext_action;
static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) {
parser::no_undef_id_error_scope scope(p);
expr e = p.parse_expr(std::numeric_limits<unsigned>::max());
expr e = p.parse_expr(LEAN_APPLY_RBP);
return p.save_pos(mk_apply_tactic_macro(e), pos);
}

7
tests/lean/run/beginend2.lean
View file

@ -6,8 +6,7 @@ open path (induction_on)
definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
(whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') :=
begin
apply (induction_on b),
apply (induction_on a),
apply ((concat_1p _)^),
apply induction_on b,
apply induction_on a,
apply (concat_1p _)^,
end
exit

2
tests/lean/run/tactic28.lean
View file

@ -12,7 +12,7 @@ theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A
theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B)
:= inhabited.destruct H (λ b, inhabited.mk (sum.inr A b))
infixl `..`:100 := append
infixl `..`:10 := append
definition my_tac := repeat (trace "iteration"; state;
( apply @inl_inhabited; trace "used inl"