From 8917e0825120affbf96268520c164212e685be5f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Apr 2021 16:18:40 -0700 Subject: [PATCH] feat: add tactic macro `unhygienic ` --- src/Init/Notation.lean | 2 ++ tests/lean/hygienicIntro.lean | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index f84e9ca24c..71bd756ec6 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -310,6 +310,8 @@ macro_rules | `(tactic| trivial) => `(tactic| contradiction) macro_rules | `(tactic| trivial) => `(tactic| apply True.intro) macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial) +macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t:tacticSeq) + end Tactic namespace Attr diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean index d8c808d97c..f3648e2db7 100644 --- a/tests/lean/hygienicIntro.lean +++ b/tests/lean/hygienicIntro.lean @@ -45,3 +45,8 @@ example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by match h₂ with | Or.inl _ => apply h₁; assumption | Or.inr h => exact h + +example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by unhygienic + cases h₂ + { apply h₁; exact h } -- hygiene is disabled + exact h