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

fix: Remove duplicate syntax definitions for mvcgen* (#9505)

Browse source 
This PR removes vestigial syntax definitions in
`Lean.Elab.Tactic.Do.VCGen` that when imported undefine the `mvcgen`
tactic. Now it should be possible to import Mathlib and still use
`mvcgen`.
This commit is contained in:
Sebastian Graf 2025-07-24 08:57:00 +02:00 • committed by GitHub
parent d8f9463af3
commit 4fdf74500d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Tactic/Do/VCGen.lean
View file

@ -96,15 +96,6 @@ def liftSimpM (x : SimpM α) : VCGenM α := do
instance : MonadLift SimpM VCGenM where
monadLift x := liftSimpM x
syntax (name := mvcgen_step) "mvcgen_step" optConfig
(num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
syntax (name := mvcgen_no_trivial) "mvcgen_no_trivial" optConfig
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
syntax (name := mvcgen) "mvcgen" optConfig
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
private def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do
let config ← elabConfig optConfig
let mut specThms ← getSpecTheorems