max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: replace constant with opaque

Browse source
This commit is contained in:
larsk21 2022-07-07 17:12:34 +02:00 • committed by Sebastian Ullrich
parent 15f9c0585a
commit 9fcae6ffe9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Linter/Basic.lean
View file

@ -99,7 +99,7 @@ def unusedVariables : Linter := fun stx => do
isInStructure,
isInInductive,
isInCtorOrStructBinder,
isInConstantOrAxiom,
isInOpaqueOrAxiom,
isInDefWithForeignDefinition,
isInDepArrow
]
@ -169,7 +169,7 @@ where
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
(stack.get? 4 |>.any fun (stx, _) =>
[``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
isInOpaqueOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
(stack.get? 4 |>.any fun (stx, _) =>
[``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))