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

chore: add tactic' => ... which preserves the conv goal annotation

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-03 19:41:39 -07:00
parent 6988560177
commit de455a9010
2 changed files with 10 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Conv.lean
View file

@ -18,20 +18,20 @@ syntax convSeq := convSeq1Indented <|> convSeqBracketed
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
syntax (name := skip) "skip" : conv
syntax (name := done) "done" : conv
syntax (name := lhs) "lhs" : conv
syntax (name := rhs) "rhs" : conv
syntax (name := whnf) "whnf" : conv
syntax (name := congr) "congr" : conv
syntax (name := arg) "arg " num : conv
syntax (name := traceState) "traceState" : conv
syntax (name := ext) "ext " (colGt ident)* : conv
syntax (name := change) "change " term : conv
syntax (name := pattern) "pattern " term : conv
syntax (name := rewrite) "rewrite " rwRuleSeq : conv
syntax (name := erewrite) "erewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
/-- Execute the given tactic block without converting `conv` goal into a regular goal -/
syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
/-- Convert the `conv` goal `⊢ lhs` into a regular goal `⊢ lhs = rhs`, and then execute the given tactic block. -/
syntax (name := nestedTactic) "tactic" " => " tacticSeq : conv
syntax (name := nestedConv) convSeqBracketed : conv
syntax (name := paren) "(" convSeq ")" : conv
@ -52,4 +52,8 @@ macro_rules
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
macro "skip" : conv => `(tactic' => rfl)
macro "done" : conv => `(tactic' => done)
macro "traceState" : conv => `(tactic' => traceState)
end Lean.Parser.Tactic.Conv

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

@ -68,11 +68,6 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
liftMetaTactic1 fun mvarId => do
replaceTargetDefEq mvarId (mkLHSGoal (← mkEq lhs' rhs))
@[builtinTactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun stx => do
liftMetaTactic1 fun mvarId => do
applyRefl mvarId
return none
@[builtinTactic Lean.Parser.Tactic.Conv.whnf] def evalWhnf : Tactic := fun stx =>
withMainContext do
let lhs ← getLhs
@ -98,11 +93,9 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
@[builtinTactic Lean.Parser.Tactic.Conv.paren] def evalParen : Tactic := fun stx =>
evalTactic stx[1]
@[builtinTactic Lean.Parser.Tactic.Conv.done] def evalDone : Tactic := fun _ =>
done
@[builtinTactic Lean.Parser.Tactic.Conv.traceState] def evalTraceState : Tactic :=
Tactic.evalTraceState
@[builtinTactic Lean.Parser.Tactic.Conv.nestedTacticCore] def evalNestedTacticCore : Tactic := fun stx => do
let seq := stx[2]
focus <| evalTactic seq
@[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
let seq := stx[2]