Skip to content

Commit d1ab525

Browse files
digama0digama0
committed
chore: simp with clauses are no longer needed (#409)
Some mathport syntax cleanup: * use `simpArgs` instead of `[simpArg,*]` * use `dsimpArg` / `dsimpArgs` instead of `simpArg` (excludes `*`) for consistency with core * remove `simp'`, `dsimp'` which are no longer needed since all features exist upstream * mark `rw_search` as "skip" since it is no longer attested in mathlib * remove `squeeze_simp`, it overlaps with `simp?` in functionality so we'll just make one thing that does both
1 parent df8292b commit d1ab525

File tree

7 files changed

+64
-99
lines changed

7 files changed

+64
-99
lines changed

‎Mathlib/Mathport/Syntax.lean‎

Lines changed: 24 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -190,12 +190,8 @@ syntax caseArg := binderIdent,+ (" :" (ppSpace (ident <|> "_"))+)?
190190
/- E -/ syntax (name := eConstructor) "econstructor" : tactic
191191
/- M -/ syntax (name := constructorM) "constructorm" "*"? ppSpace term,* : tactic
192192
/- M -/ syntax (name := injections') "injections" (" with " (colGt (ident <|> "_"))+)? : tactic
193-
/- N -/ syntax (name := simp') "simp'" "*"? (config)? (discharger)? (&" only")?
194-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
195193
/- N -/ syntax (name := simpIntro) "simp_intro" (config)?
196-
(ppSpace colGt (ident <|> "_"))* (&" only")? (" [" simpArg,* "]")? (" with " ident+)? : tactic
197-
/- N -/ syntax (name := dsimp') "dsimp'" (config)? (&" only")?
198-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
194+
(ppSpace colGt (ident <|> "_"))* (&" only")? (simpArgs)? : tactic
199195
/- E -/ syntax (name := symm) "symm" : tactic
200196
/- E -/ syntax (name := trans) "trans" (ppSpace colGt term)? : tactic
201197
/- B -/ syntax (name := cc) "cc" : tactic
@@ -222,10 +218,7 @@ namespace Conv
222218

223219
open Tactic (simpArg rwRuleSeq)
224220
/- N -/ syntax (name := «for») "for " term:max " [" num,* "]" " => " tacticSeq : conv
225-
/- N -/ syntax (name := simp') "simp'" (config)? (discharger)? (&" only")?
226-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? : conv
227-
/- N -/ syntax (name := dsimp) "dsimp" (config)? (&" only")?
228-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? : conv
221+
/- N -/ syntax (name := dsimp) "dsimp" (config)? (&" only")? (dsimpArgs)? : conv
229222
/- E -/ syntax (name := guardLHS) "guard_lhs " " =ₐ " term : conv
230223

231224
end Conv
@@ -297,11 +290,11 @@ end Conv
297290
/- M -/ syntax (name := unelide) "unelide" (ppSpace location)? : tactic
298291

299292
/- S -/ syntax (name := clarify) "clarify" (config)?
300-
(" [" Parser.Tactic.simpArg,* "]")? (" using " term,+)? : tactic
293+
(Parser.Tactic.simpArgs)? (" using " term,+)? : tactic
301294
/- S -/ syntax (name := safe) "safe" (config)?
302-
(" [" Parser.Tactic.simpArg,* "]")? (" using " term,+)? : tactic
295+
(Parser.Tactic.simpArgs)? (" using " term,+)? : tactic
303296
/- S -/ syntax (name := finish) "finish" (config)?
304-
(" [" Parser.Tactic.simpArg,* "]")? (" using " term,+)? : tactic
297+
(Parser.Tactic.simpArgs)? (" using " term,+)? : tactic
305298

306299
syntax generalizesArg := (ident " : ")? term:51 " = " ident
307300
/- M -/ syntax (name := generalizes) "generalizes " "[" generalizesArg,* "]" : tactic
@@ -332,37 +325,27 @@ syntax termList := " [" term,* "]"
332325

333326
/- M -/ syntax (name := assocRw) "assoc_rw " rwRuleSeq (ppSpace location)? : tactic
334327

335-
/- N -/ syntax (name := dsimpResult) "dsimp_result " (&"only ")? ("[" Tactic.simpArg,* "]")?
336-
(" with " ident+)? " => " tacticSeq : tactic
337-
/- N -/ syntax (name := simpResult) "simp_result " (&"only ")? ("[" Tactic.simpArg,* "]")?
338-
(" with " ident+)? " => " tacticSeq : tactic
328+
/- N -/ syntax (name := dsimpResult) "dsimp_result "
329+
(&"only ")? (dsimpArgs)? " => " tacticSeq : tactic
330+
/- N -/ syntax (name := simpResult) "simp_result "
331+
(&"only ")? (simpArgs)? " => " tacticSeq : tactic
339332

340333
/- M -/ syntax (name := splitIfs) "split_ifs" (ppSpace location)? (" with " binderIdent+)? : tactic
341334

342335
/- S -/ syntax (name := squeezeScope) "squeeze_scope " tacticSeq : tactic
343336

344-
syntax squeezeSimpArgsRest := (config)? (discharger)? (&" only")?
345-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)?
346-
/- S -/ syntax "squeeze_simp" "!"? "?"? squeezeSimpArgsRest : tactic
347-
macro "squeeze_simp?" rest:squeezeSimpArgsRest : tactic =>
348-
`(tactic| squeeze_simp ? $rest:squeezeSimpArgsRest)
349-
macro "squeeze_simp!" rest:squeezeSimpArgsRest : tactic =>
350-
`(tactic| squeeze_simp ! $rest:squeezeSimpArgsRest)
351-
macro "squeeze_simp!?" rest:squeezeSimpArgsRest : tactic =>
352-
`(tactic| squeeze_simp !? $rest:squeezeSimpArgsRest)
353-
354-
syntax squeezeDSimpArgsRest := (config)? (&" only")?
355-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)?
356-
/- S -/ syntax "squeeze_dsimp" "!"? "?"? squeezeDSimpArgsRest : tactic
357-
macro "squeeze_dsimp?" rest:squeezeDSimpArgsRest : tactic =>
358-
`(tactic| squeeze_dsimp ? $rest:squeezeDSimpArgsRest)
359-
macro "squeeze_dsimp!" rest:squeezeDSimpArgsRest : tactic =>
360-
`(tactic| squeeze_dsimp ! $rest:squeezeDSimpArgsRest)
361-
macro "squeeze_dsimp!?" rest:squeezeDSimpArgsRest : tactic =>
362-
`(tactic| squeeze_dsimp !? $rest:squeezeDSimpArgsRest)
337+
syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
338+
syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)? (ppSpace location)?
339+
syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
340+
/- S -/ syntax "simp?" "!"? simpTraceArgsRest : tactic
341+
/- S -/ syntax "simp_all?" "!"? simpAllTraceArgsRest : tactic
342+
/- S -/ syntax "dsimp?" "!"? dsimpTraceArgsRest : tactic
343+
macro "simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp? ! $rest)
344+
macro "simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all? ! $rest)
345+
macro "dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp? ! $rest)
363346

364347
/- S -/ syntax (name := suggest) "suggest" (config)? (ppSpace num)?
365-
(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " (colGt binderIdent)+)? : tactic
348+
(simpArgs)? (" using " (colGt binderIdent)+)? : tactic
366349

367350
/- B -/ syntax (name := tauto) "tauto" (config)? : tactic
368351
/- B -/ syntax (name := tauto!) "tauto!" (config)? : tactic
@@ -432,14 +415,14 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
432415

433416
/- M -/ syntax (name := cancelDenoms) "cancel_denoms" (ppSpace location)? : tactic
434417

435-
/- M -/ syntax (name := zify) "zify" (" [" simpArg,* "]")? (ppSpace location)? : tactic
418+
/- M -/ syntax (name := zify) "zify" (simpArgs)? (ppSpace location)? : tactic
436419

437420
/- S -/ syntax (name := transport) "transport" (ppSpace term)? " using " term : tactic
438421

439422
/- M -/ syntax (name := unfoldCases) "unfold_cases " tacticSeq : tactic
440423

441424
/- M -/ syntax (name := fieldSimp) "field_simp" (config)? (discharger)? (&" only")?
442-
(" [" Tactic.simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
425+
(Tactic.simpArgs)? (ppSpace location)? : tactic
443426

444427
/- B -/ syntax (name := equivRw) "equiv_rw" (config)? (termList <|> term) (ppSpace location)? : tactic
445428
/- B -/ syntax (name := equivRwType) "equiv_rw_type" (config)? term : tactic
@@ -496,7 +479,7 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
496479
/- M -/ syntax (name := ghostFunTac) "ghost_fun_tac " term ", " term : tactic
497480
/- M -/ syntax (name := ghostCalc) "ghost_calc" (ppSpace binderIdent)* : tactic
498481
/- M -/ syntax (name := initRing) "init_ring" (" using " term)? : tactic
499-
/- E -/ syntax (name := ghostSimp) "ghost_simp" (" [" simpArg,* "]")? : tactic
482+
/- E -/ syntax (name := ghostSimp) "ghost_simp" (simpArgs)? : tactic
500483
/- E -/ syntax (name := wittTruncateFunTac) "witt_truncate_fun_tac" : tactic
501484

502485
/- M -/ @[nolint docBlame] syntax (name := pure_coherence) "pure_coherence" : tactic
@@ -510,7 +493,7 @@ namespace Conv
510493
/- E -/ syntax (name := guardTarget) "guard_target" " =ₐ " term : conv
511494

512495
/- E -/ syntax (name := normNum1) "norm_num1" : conv
513-
/- E -/ syntax (name := normNum) "norm_num" (" [" simpArg,* "]")? : conv
496+
/- E -/ syntax (name := normNum) "norm_num" (simpArgs)? : conv
514497

515498
/- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? : conv
516499
/- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? : conv
@@ -585,8 +568,7 @@ macro_rules
585568

586569
/- N -/ syntax (name := defReplacer) "def_replacer " ident Term.optType : command
587570

588-
/- S -/ syntax (name := simp) "#simp" (&" only")? (" [" Tactic.simpArg,* "]")?
589-
(" with " ident+)? " :"? ppSpace term : command
571+
/- S -/ syntax (name := simp) "#simp" (&" only")? (Tactic.simpArgs)? " :"? ppSpace term : command
590572

591573
/- S -/ syntax (name := «where») "#where" : command
592574

‎Mathlib/Tactic/Core.lean‎

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -65,24 +65,33 @@ namespace Parser.Tactic
6565
-- syntax simpArg := simpStar <|> simpErase <|> simpLemma
6666
def simpArg := simpStar.binary `orelse (simpErase.binary `orelse simpLemma)
6767

68-
syntax simpArgs := " [" simpArg,* "] "
68+
-- syntax dsimpArg := simpErase <|> simpLemma
69+
def dsimpArg := simpErase.binary `orelse simpLemma
70+
71+
syntax simpArgs := " [" simpArg,* "]"
72+
syntax dsimpArgs := " [" dsimpArg,* "]"
6973
syntax withArgs := " with " (colGt ident)+
7074
syntax usingArg := " using " term
7175

7276
/-- Extract the arguments from a `simpArgs` syntax as an array of syntaxes -/
7377
def getSimpArgs : Syntax → TacticM (Array Syntax)
74-
| `(simpArgs|[$args,*]) => pure args.getElems
75-
| _ => Elab.throwUnsupportedSyntax
78+
| `(simpArgs| [$args,*]) => pure args.getElems
79+
| _ => Elab.throwUnsupportedSyntax
80+
81+
/-- Extract the arguments from a `dsimpArgs` syntax as an array of syntaxes -/
82+
def getDSimpArgs : Syntax → TacticM (Array Syntax)
83+
| `(dsimpArgs| [$args,*]) => pure args.getElems
84+
| _ => Elab.throwUnsupportedSyntax
7685

7786
/-- Extract the arguments from a `withArgs` syntax as an array of syntaxes -/
7887
def getWithArgs : Syntax → TacticM (Array Syntax)
79-
| `(withArgs|with $args*) => pure args
80-
| _ => Elab.throwUnsupportedSyntax
88+
| `(withArgs| with $args*) => pure args
89+
| _ => Elab.throwUnsupportedSyntax
8190

8291
/-- Extract the argument from a `usingArg` syntax as a syntax term -/
8392
def getUsingArg : Syntax → TacticM Syntax
84-
| `(usingArg|using $e) => pure e
85-
| _ => Elab.throwUnsupportedSyntax
93+
| `(usingArg| using $e) => pure e
94+
| _ => Elab.throwUnsupportedSyntax
8695

8796
/--
8897
`repeat1 tac` applies `tac` to main goal at least once. If the application succeeds,

‎Mathlib/Tactic/LibrarySearch.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -99,10 +99,10 @@ open Lean.Parser.Tactic
9999
-- in particular including additional lemmas
100100
-- with `library_search [X, Y, Z]` or `library_search with attr`,
101101
-- or requiring that a particular hypothesis is used in the solution, with `library_search using h`.
102-
syntax (name := librarySearch') "library_search" (config)? (" [" simpArg,* "]")?
103-
(" with " (colGt ident)+)? (" using " (colGt binderIdent)+)? : tactic
104-
syntax (name := librarySearch!) "library_search!" (config)? (" [" simpArg,* "]")?
105-
(" with " (colGt ident)+)? (" using " (colGt binderIdent)+)? : tactic
102+
syntax (name := librarySearch') "library_search" (config)? (simpArgs)?
103+
(" using " (colGt binderIdent)+)? : tactic
104+
syntax (name := librarySearch!) "library_search!" (config)? (simpArgs)?
105+
(" using " (colGt binderIdent)+)? : tactic
106106

107107
-- For now we only implement the basic functionality.
108108
-- The full syntax is recognized, but will produce a "Tactic has not been implemented" error.

‎Mathlib/Tactic/NormNum.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,7 @@ namespace Tactic
224224
open Lean.Parser.Tactic
225225

226226
/-- Normalize numerical expressions. -/
227-
elab "norm_num" args:(("[" simpArg,* "]")?) loc:(location ?) : tactic =>
227+
elab "norm_num" args:(simpArgs ?) loc:(location ?) : tactic =>
228228
withOptions (·.setBool `norm_num.nosimp false)
229229
<| Meta.NormNum.elabNormNum args loc
230230

‎Mathlib/Tactic/Simpa.lean‎

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,12 @@ namespace Mathlib.Tactic
1010

1111
open Lean Parser.Tactic Elab.Tactic
1212

13-
syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (withArgs)? (usingArg)?
13+
syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (usingArg)?
1414

15-
syntax "simpa" "!"? "?"? simpaArgsRest : tactic
15+
syntax "simpa" "?"? "!"? simpaArgsRest : tactic
1616
macro "simpa!" rest:simpaArgsRest : tactic => `(tactic| simpa ! $rest:simpaArgsRest)
1717
macro "simpa?" rest:simpaArgsRest : tactic => `(tactic| simpa ? $rest:simpaArgsRest)
18-
macro "simpa!?" rest:simpaArgsRest : tactic => `(tactic| simpa !? $rest:simpaArgsRest)
19-
20-
-- TODO
21-
syntax "squeeze_simpa" "!"? "?"? simpaArgsRest : tactic
22-
macro "squeeze_simpa!" rest:simpaArgsRest : tactic => `(tactic| squeeze_simpa ! $rest:simpaArgsRest)
23-
macro "squeeze_simpa?" rest:simpaArgsRest : tactic => `(tactic| squeeze_simpa ? $rest:simpaArgsRest)
24-
macro "squeeze_simpa!?" rest:simpaArgsRest : tactic => `(tactic| squeeze_simpa !? $rest:simpaArgsRest)
18+
macro "simpa?!" rest:simpaArgsRest : tactic => `(tactic| simpa ?! $rest:simpaArgsRest)
2519

2620
/--
2721
This is a "finishing" tactic modification of `simp`. It has two forms.
@@ -42,8 +36,8 @@ This is a "finishing" tactic modification of `simp`. It has two forms.
4236
#TODO: implement `?`
4337
-/
4438
elab_rules : tactic
45-
| `(tactic| simpa $[!%$unfold]? $[?%$squeeze]? $[$cfg:config]? $[$disch:discharger]? $[only%$only]?
46-
$[[$args,*]]? $[with $wth]? $[using $usingArg]?) => do
39+
| `(tactic| simpa $[?%$squeeze]? $[!%$unfold]? $[$cfg:config]? $[$disch:discharger]? $[only%$only]?
40+
$[[$args,*]]? $[using $usingArg]?) => do
4741
let nGoals := (← getUnsolvedGoals).length
4842
evalTactic $ ← `(tactic|simp $(cfg)? $(disch)? $[only%$only]? $[[$[$args],*]]?)
4943
if (← getUnsolvedGoals).length < nGoals then

‎Mathlib/Tactic/SolveByElim.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,7 @@ namespace Lean.Tactic
2929

3030
open Lean.Parser.Tactic
3131

32-
syntax (name := solveByElim) "solve_by_elim" "*"? (config)?
33-
(&" only")? (" [" simpArg,* "]")? (" with " (colGt ident)+)? : tactic
32+
syntax (name := solveByElim) "solve_by_elim" "*"? (config)? (&" only")? (simpArgs)? : tactic
3433

3534
elab_rules : tactic | `(tactic| solve_by_elim) => do withMainContext do
3635
Meta.solveByElim 6 (← getMainGoal)

‎scripts/nolints.json‎

Lines changed: 13 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -158,20 +158,9 @@
158158
["docBlame", "LinearOrder.le_total"],
159159
["docBlame", "List.card"],
160160
["docBlame", "List.equiv"],
161-
["docBlame", "List.findIdx?"],
162-
["docBlame", "List.indexOf?"],
163161
["docBlame", "List.inj_on"],
164-
["docBlame", "List.mmap"],
165-
["docBlame", "List.mmap'"],
166162
["docBlame", "List.remove"],
167-
["docBlame", "List.sublists'Aux"],
168-
["docBlame", "List.sublistsAux"],
169-
["docBlame", "List.sublistsAux₁"],
170-
["docBlame", "List.«term_<+:_»"],
171-
["docBlame", "List.«term_<:+:_»"],
172-
["docBlame", "List.«term_<:+_»"],
173163
["docBlame", "List.«term_~_»"],
174-
["docBlame", "List.traverse"],
175164
["docBlame", "MonadWriter.listen"],
176165
["docBlame", "MonadWriter.pass"],
177166
["docBlame", "MonadWriter.tell"],
@@ -343,14 +332,10 @@
343332
["docBlame", "Mathlib.Tactic.tacticLet_"],
344333
["docBlame", "Mathlib.Tactic.tacticRight"],
345334
["docBlame", "Mathlib.Tactic.tacticSet!_"],
346-
["docBlame", "Mathlib.Tactic.tacticSimpa!?_"],
347-
["docBlame", "Mathlib.Tactic.tacticSimpa!?__1"],
348335
["docBlame", "Mathlib.Tactic.tacticSimpa!_"],
336+
["docBlame", "Mathlib.Tactic.tacticSimpa?!_"],
337+
["docBlame", "Mathlib.Tactic.tacticSimpa?!__1"],
349338
["docBlame", "Mathlib.Tactic.tacticSimpa?_"],
350-
["docBlame", "Mathlib.Tactic.tacticSqueeze_simpa!?_"],
351-
["docBlame", "Mathlib.Tactic.tacticSqueeze_simpa!?__1"],
352-
["docBlame", "Mathlib.Tactic.tacticSqueeze_simpa!_"],
353-
["docBlame", "Mathlib.Tactic.tacticSqueeze_simpa?_"],
354339
["docBlame", "Mathlib.Tactic.tacticSuffices_"],
355340
["docBlame", "Mathlib.WhatsNew.diffExtension"],
356341
["docBlame", "Mathlib.WhatsNew.whatsNew"],
@@ -529,16 +514,17 @@
529514
["docBlame", "Lean.Parser.Tactic.deltaInstance"],
530515
["docBlame", "Lean.Parser.Tactic.deriveElementwiseProof"],
531516
["docBlame", "Lean.Parser.Tactic.deriveReassocProof"],
532-
["docBlame", "Lean.Parser.Tactic.dsimp'"],
517+
["docBlame", "Lean.Parser.Tactic.dsimpArg"],
518+
["docBlame", "Lean.Parser.Tactic.dsimpArgs"],
533519
["docBlame", "Lean.Parser.Tactic.dsimpResult"],
520+
["docBlame", "Lean.Parser.Tactic.dsimpTraceArgsRest"],
534521
["docBlame", "Lean.Parser.Tactic.eConstructor"],
535522
["docBlame", "Lean.Parser.Tactic.eapply'"],
536523
["docBlame", "Lean.Parser.Tactic.elementwise"],
537524
["docBlame", "Lean.Parser.Tactic.elementwise!"],
538525
["docBlame", "Lean.Parser.Tactic.elide"],
539526
["docBlame", "Lean.Parser.Tactic.equivRw"],
540527
["docBlame", "Lean.Parser.Tactic.equivRwType"],
541-
["docBlame", "Lean.Parser.Tactic.existsi"],
542528
["docBlame", "Lean.Parser.Tactic.extractGoal"],
543529
["docBlame", "Lean.Parser.Tactic.extractGoal!"],
544530
["docBlame", "Lean.Parser.Tactic.failIfSuccess?"],
@@ -629,30 +615,27 @@
629615
["docBlame", "Lean.Parser.Tactic.rwSearch"],
630616
["docBlame", "Lean.Parser.Tactic.rwSearch?"],
631617
["docBlame", "Lean.Parser.Tactic.safe"],
632-
["docBlame", "Lean.Parser.Tactic.simp'"],
618+
["docBlame", "Lean.Parser.Tactic.simpAllTraceArgsRest"],
633619
["docBlame", "Lean.Parser.Tactic.simpArg"],
634620
["docBlame", "Lean.Parser.Tactic.simpArgs"],
635621
["docBlame", "Lean.Parser.Tactic.simpIntro"],
636622
["docBlame", "Lean.Parser.Tactic.simpResult"],
623+
["docBlame", "Lean.Parser.Tactic.simpTraceArgsRest"],
637624
["docBlame", "Lean.Parser.Tactic.sliceLHS"],
638625
["docBlame", "Lean.Parser.Tactic.sliceRHS"],
639626
["docBlame", "Lean.Parser.Tactic.splitIfs"],
640-
["docBlame", "Lean.Parser.Tactic.squeezeDSimpArgsRest"],
641627
["docBlame", "Lean.Parser.Tactic.squeezeScope"],
642-
["docBlame", "Lean.Parser.Tactic.squeezeSimpArgsRest"],
643628
["docBlame", "Lean.Parser.Tactic.subtypeInstance"],
644629
["docBlame", "Lean.Parser.Tactic.suggest"],
645630
["docBlame", "Lean.Parser.Tactic.symm"],
646631
["docBlame", "Lean.Parser.Tactic.symm'"],
647632
["docBlame", "Lean.Parser.Tactic.tacticDestruct_"],
648-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_dsimp!?_"],
649-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_dsimp!?__1"],
650-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_dsimp!_"],
651-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_dsimp?_"],
652-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_simp!?_"],
653-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_simp!?__1"],
654-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_simp!_"],
655-
["docBlame", "Lean.Parser.Tactic.tacticSqueeze_simp?_"],
633+
["docBlame", "Lean.Parser.Tactic.tacticDsimp?!_"],
634+
["docBlame", "Lean.Parser.Tactic.tacticDsimp?!__1"],
635+
["docBlame", "Lean.Parser.Tactic.tacticSimp?!_"],
636+
["docBlame", "Lean.Parser.Tactic.tacticSimp?!__1"],
637+
["docBlame", "Lean.Parser.Tactic.tacticSimp_all?!_"],
638+
["docBlame", "Lean.Parser.Tactic.tacticSimp_all?!__1"],
656639
["docBlame", "Lean.Parser.Tactic.tauto"],
657640
["docBlame", "Lean.Parser.Tactic.tauto!"],
658641
["docBlame", "Lean.Parser.Tactic.termList"],
@@ -665,7 +648,6 @@
665648
["docBlame", "Lean.Parser.Tactic.transport"],
666649
["docBlame", "Lean.Parser.Tactic.truncCases"],
667650
["docBlame", "Lean.Parser.Tactic.tryFor"],
668-
["docBlame", "Lean.Parser.Tactic.typeCheck"],
669651
["docBlame", "Lean.Parser.Tactic.unelide"],
670652
["docBlame", "Lean.Parser.Tactic.unfold'"],
671653
["docBlame", "Lean.Parser.Tactic.unfold1"],
@@ -731,7 +713,6 @@
731713
["docBlame", "Lean.Parser.Tactic.Conv.ringExp!"],
732714
["docBlame", "Lean.Parser.Tactic.Conv.ringNF"],
733715
["docBlame", "Lean.Parser.Tactic.Conv.ringNF!"],
734-
["docBlame", "Lean.Parser.Tactic.Conv.simp'"],
735716
["docBlame", "Lean.Parser.Tactic.Conv.slice"],
736717
["docBlame", "Lean.Parser.Tactic.ElimApp.evalNames"],
737718
["docBlame", "Lean.Parser.Tactic.mono.side"],

0 commit comments

Comments
 (0)