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

chore: use snake_case for user-facing tactic names

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-16 10:23:12 -07:00
parent 1c00f29043
commit 0a898965a3
5 changed files with 27 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Conv.lean
View file

@ -31,7 +31,7 @@ syntax (name := delta) "delta " ident : conv
syntax (name := pattern) "pattern " term : conv
syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
syntax (name := simp) "simp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := simpMatch) "simpMatch " : conv
syntax (name := simpMatch) "simp_match " : conv
/-- Execute the given tactic block without converting `conv` goal into a regular goal -/
syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
@ -59,7 +59,7 @@ macro_rules
macro "skip" : conv => `(tactic => rfl)
macro "done" : conv => `(tactic' => done)
macro "traceState" : conv => `(tactic' => traceState)
macro "trace_state" : conv => `(tactic' => trace_state)
macro "apply " e:term : conv => `(tactic => apply $e)
end Lean.Parser.Tactic.Conv

2
src/Init/Core.lean
View file

@ -934,7 +934,7 @@ protected abbrev recOnSubsingleton₂
intro a; apply s
induction q₂ using Quot.recOnSubsingleton
intro a; apply s
inferInstance
infer_instance
end
end Quotient

44
src/Init/Notation.lean
View file

@ -282,9 +282,9 @@ syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq
macro "next " args:(ident <|> "_")* " => " tac:tacticSeq : tactic => `(tactic| case _ $(args.getArgs)* => $tac)
/-- `allGoals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
syntax (name := allGoals) "allGoals " tacticSeq : tactic
syntax (name := allGoals) "all_goals " tacticSeq : tactic
/-- `anyGoals tac` applies the tactic `tac` to every goal, and succeeds if at least one application succeeds. -/
syntax (name := anyGoals) "anyGoals " tacticSeq : tactic
syntax (name := anyGoals) "any_goals " tacticSeq : tactic
/--
`focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred. -/
@ -293,19 +293,19 @@ syntax (name := focus) "focus " tacticSeq : tactic
syntax (name := skip) "skip" : tactic
/-- `done` succeeds iff there are no remaining goals. -/
syntax (name := done) "done" : tactic
syntax (name := traceState) "traceState" : tactic
syntax (name := failIfSuccess) "failIfSuccess " tacticSeq : tactic
syntax (name := traceState) "trace_state" : tactic
syntax (name := failIfSuccess) "fail_if_success " tacticSeq : tactic
syntax (name := paren) "(" tacticSeq ")" : tactic
syntax (name := withReducible) "withReducible " tacticSeq : tactic
syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
syntax (name := withReducible) "with_reducible " tacticSeq : tactic
syntax (name := withReducibleAndInstances) "with_reducible_and_instances " tacticSeq : tactic
/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
syntax (name := first) "first " withPosition((group(colGe "|" tacticSeq))+) : tactic
syntax (name := rotateLeft) "rotateLeft" (num)? : tactic
syntax (name := rotateRight) "rotateRight" (num)? : tactic
syntax (name := rotateLeft) "rotate_left" (num)? : tactic
syntax (name := rotateRight) "rotate_right" (num)? : tactic
/-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
macro "try " t:tacticSeq : tactic => `(first | $t | skip)
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/
macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_goals $y:tactic))
/-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
macro dot:("·" <|> ".") ts:tacticSeq : tactic => `(tactic| {%$dot ($ts:tacticSeq) })
@ -316,7 +316,7 @@ macro "rfl" : tactic => `(exact rfl)
macro "admit" : tactic => `(exact sorry)
/-- The `sorry` tactic isnxo a shorthand for `exact sorry`. -/
macro "sorry" : tactic => `(exact sorry)
macro "inferInstance" : tactic => `(exact inferInstance)
macro "infer_instance" : tactic => `(exact inferInstance)
/-- Optional configuration option for tactics -/
syntax config := atomic("(" &"config") " := " term ")"
@ -343,7 +343,7 @@ def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Sy
-- Replace `]` token with one without position information in the expanded tactic
let seq := seq.setArg 2 (mkAtom "]")
let tac := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 2 seq
`(tactic| $tac; try (withReducible rfl%$rbrak))
`(tactic| $tac; try (with_reducible rfl%$rbrak))
@[macro rwSeq] def expandRwSeq : Macro :=
rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
@ -369,23 +369,23 @@ syntax (name := delta) "delta " ident (location)? : tactic
-- Auxiliary macro for lifting have/suffices/let/...
-- It makes sure the "continuation" `?_` is the main goal after refining
macro "refineLift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotateRight))
macro "refine_lift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotate_right))
macro "have " d:haveDecl : tactic => `(refineLift have $d:haveDecl; ?_)
macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
/- We use a priority > default, to avoid ambiguity with previous `have` notation -/
macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
macro "suffices " d:sufficesDecl : tactic => `(refineLift suffices $d:sufficesDecl; ?_)
macro "let " d:letDecl : tactic => `(refineLift let $d:letDecl; ?_)
macro "show " e:term : tactic => `(refineLift show $e:term from ?_)
macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d:sufficesDecl; ?_)
macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
macro "show " e:term : tactic => `(refine_lift show $e:term from ?_)
syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
macro_rules
| `(tactic| let rec $d:letRecDecls) => `(tactic| refineLift let rec $d:letRecDecls; ?_)
| `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
-- Similar to `refineLift`, but using `refine'`
macro "refineLift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotateRight))
macro "have' " d:haveDecl : tactic => `(refineLift' have $d:haveDecl; ?_)
macro "refine_lift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotate_right))
macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
macro "let' " d:letDecl : tactic => `(refineLift' let $d:letDecl; ?_)
macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
syntax inductionAlt := "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
@ -402,8 +402,8 @@ syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)
syntax (name := existsIntro) "exists " term : tactic
/-- `renameI x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
syntax (name := renameI) "renameI " (colGt (ident <|> "_"))+ : tactic
/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
syntax (name := renameI) "rename_i " (colGt (ident <|> "_"))+ : tactic
syntax "repeat " tacticSeq : tactic
macro_rules

2
src/Lean/Elab/Tactic/BuiltinTactic.lean
View file

@ -269,7 +269,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
| _ => throwUnsupportedSyntax
@[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
| stx@`(tactic| renameI $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
| stx@`(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
| _ => throwUnsupportedSyntax
@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do

2
src/Lean/Elab/Tactic/Conv/Basic.lean
View file

@ -88,7 +88,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
-- save state before/after entering focus on `{`
withInfoContext (pure ()) initInfo
evalManyTacticOptSemi stx[1]
evalTactic (← `(tactic| allGoals (try rfl)))
evalTactic (← `(tactic| all_goals (try rfl)))
@[builtinTactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
evalConvSeqBracketed stx[0]