We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent eed0293 commit 01bdc70Copy full SHA for 01bdc70
src/Lean/AuxRecursor.lean
@@ -84,7 +84,7 @@ def markNoConfusion (env : Environment) (n : Name) (info : NoConfusionInfo) : En
84
noConfusionExt.insert env n info
85
86
def isNoConfusion (env : Environment) (n : Name) : Bool :=
87
- (noConfusionExt.find? env n).isSome
+ noConfusionExt.contains env n
88
89
def getNoConfusionInfo (env : Environment) (n : Name) : NoConfusionInfo :=
90
(noConfusionExt.find? env n).get!
0 commit comments