Skip to content

Commit 53e6e99

Browse files
authored
refactor: generalize addMatcherInfo (#5068)
works in any `MonadEnv`.
1 parent 59ca274 commit 53e6e99

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Meta/Match/MatcherInfo.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo :
9292

9393
end Extension
9494

95-
def addMatcherInfo (matcherName : Name) (info : MatcherInfo) : MetaM Unit :=
95+
def addMatcherInfo [Monad m] [MonadEnv m] (matcherName : Name) (info : MatcherInfo) : m Unit :=
9696
modifyEnv fun env => Extension.addMatcherInfo env matcherName info
9797

9898
end Match

0 commit comments

Comments
 (0)