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

chore: fix namespaces in recently upstreamed tactics (#3672)

Browse source
This commit is contained in:
Scott Morrison 2024-03-17 17:41:40 +11:00 • committed by GitHub
parent 8e96d7ba1d
commit 88b1751b54
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/ShowTerm.lean
View file

@ -7,7 +7,7 @@ prelude
import Lean.Elab.ElabRules
import Lean.Meta.Tactic.TryThis
namespace Std.Tactic
namespace Lean.Elab.Tactic.ShowTerm
open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
@[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
@ -26,3 +26,5 @@ open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
pure e
| _, _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.ShowTerm

4
src/Lean/Elab/Tactic/Simpa.lean
View file

@ -18,7 +18,7 @@ register_option linter.unnecessarySimpa : Bool := {
descr := "enable the 'unnecessary simpa' linter"
}
namespace Std.Tactic.Simpa
namespace Lean.Elab.Tactic.Simpa
open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
@ -86,3 +86,5 @@ deriving instance Repr for UseImplicitLambdaResult
| _ => unreachable!
TryThis.addSuggestion tk stx (origSpan? := ← getRef)
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Simpa