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

fix: conv case => should close the goal conv-style

Browse source
This commit is contained in:
Mario Carneiro 2022-09-27 19:43:34 -04:00 • committed by Leonardo de Moura
parent 6f8e861158
commit 2a748d3035
1 changed files with 22 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/Init/Conv.lean
View file

@ -167,6 +167,27 @@ syntax (name := nestedConv) convSeqBracketed : conv
This is pure grouping with no added effects. -/
syntax (name := paren) "(" convSeq ")" : conv
/-- `rfl` closes one conv goal "trivially", by using reflexivity
(that is, no rewriting). -/
macro "rfl" : conv => `(tactic => rfl)
/-- `done` succeeds iff there are no goals remaining. -/
macro "done" : conv => `(tactic' => done)
/-- `trace_state` prints the current goal state. -/
macro "trace_state" : conv => `(tactic' => trace_state)
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
macro (name := allGoals) tk:"all_goals " s:convSeq : conv =>
`(conv| tactic' => all_goals%$tk conv' => $s)
/--
`any_goals tac` applies the tactic `tac` to every goal, and succeeds if at
least one application succeeds.
-/
macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
`(conv| tactic' => any_goals%$tk conv' => $s)
/--
* `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
or else fails.
@ -175,7 +196,7 @@ syntax (name := paren) "(" convSeq ")" : conv
* `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
-/
macro (name := case) tk:"case " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
`(conv| tactic' => case%$tk $args|* =>%$arr conv' => $s)
`(conv| tactic' => case%$tk $args|* =>%$arr conv' => ($s); all_goals rfl)
/--
`case'` is similar to the `case tag => tac` tactic, but does not ensure the goal
@ -193,17 +214,6 @@ inaccessible names to the given names.
-/
macro "next " args:binderIdent* " => " tac:convSeq : conv => `(conv| case _ $args* => $tac)
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
macro (name := allGoals) tk:"all_goals " s:convSeq : conv =>
`(conv| tactic' => all_goals%$tk conv' => $s)
/--
`any_goals tac` applies the tactic `tac` to every goal, and succeeds if at
least one application succeeds.
-/
macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
`(conv| tactic' => any_goals%$tk conv' => $s)
/--
`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.
@ -256,16 +266,6 @@ macro_rules
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
/-- `rfl` closes one conv goal "trivially", by using reflexivity
(that is, no rewriting). -/
macro "rfl" : conv => `(tactic => rfl)
/-- `done` succeeds iff there are no goals remaining. -/
macro "done" : conv => `(tactic' => done)
/-- `trace_state` prints the current goal state. -/
macro "trace_state" : conv => `(tactic' => trace_state)
/-- The `apply thm` conv tactic is the same as `apply thm` the tactic.
There are no restrictions on `thm`, but strange results may occur if `thm`
cannot be reasonably interpreted as proving one equality from a list of others. -/