From b3f562d6c1177c98e9b30f1abd858ff3f5eb318f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 23 Aug 2024 04:17:40 +0000 Subject: [PATCH] feat: toAdditive to transfer MatcherInfo data (#16026) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074 --- Mathlib/Tactic/ToAdditive/Frontend.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean index f1201fe61ce4c..e62da2bc7ca03 100644 --- a/Mathlib/Tactic/ToAdditive/Frontend.lean +++ b/Mathlib/Tactic/ToAdditive/Frontend.lean @@ -13,6 +13,7 @@ import Mathlib.Lean.Name import Lean.Elab.Tactic.Ext import Lean.Meta.Tactic.Symm import Lean.Meta.Tactic.Rfl +import Lean.Meta.Match.MatcherInfo import Batteries.Lean.NameMapAttribute import Batteries.Tactic.Lint -- useful to lint this file and for for DiscrTree.elements import Mathlib.Tactic.Relation.Trans -- just to copy the attribute @@ -816,6 +817,11 @@ partial def transformDeclAux selectionRange := ← getDeclarationRange cfg.ref } if isProtected (← getEnv) src then setEnv <| addProtected (← getEnv) tgt + if let some matcherInfo ← getMatcherInfo? src then + -- Use + -- Match.addMatcherInfo tgt matcherInfo + -- once on lean 4.13. + modifyEnv fun env => Match.Extension.addMatcherInfo env tgt matcherInfo /-- Copy the instance attribute in a `to_additive`