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

feat: let conv tactics ext/intro/enter take _ (#7806)

Browse source 
This PR modifies the syntaxes of the `ext`, `intro` and `enter` conv
tactics to accept `_`. The introduced binder is an inaccessible name.
This commit is contained in:
Kyle Miller 2025-04-03 17:01:29 -07:00 • committed by GitHub
parent edf88cc5be
commit 092ece5d49
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Conv.lean
View file

@ -97,7 +97,7 @@ syntax (name := arg) "arg " argArg : conv
/-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
to target `e`, introducing name `x` in the process. -/
syntax (name := ext) "ext" (ppSpace colGt ident)* : conv
syntax (name := ext) "ext" (ppSpace colGt binderIdent)* : conv
/-- `change t'` replaces the target `t` with `t'`,
assuming `t` and `t'` are definitionally equal. -/
@ -281,9 +281,9 @@ macro "left" : conv => `(conv| lhs)
/-- `right` traverses into the right argument. Synonym for `rhs`. -/
macro "right" : conv => `(conv| rhs)
/-- `intro` traverses into binders. Synonym for `ext`. -/
macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*)
macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
syntax enterArg := ident <|> argArg
syntax enterArg := binderIdent <|> argArg
/-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:

10
src/Lean/Elab/Tactic/Conv/Congr.lean
View file

@ -318,7 +318,11 @@ private def ext (userName? : Option Name) : TacticM Unit := do
ext none
else
for id in ids do
withRef id <| ext id.getId
let userName? :=
match id with
| `(binderIdent| $id:ident) => some id.getId
| _ => none
withRef id <| ext userName?
-- syntax (name := enter) "enter" " [" enterArg,+ "]" : conv
@[builtin_tactic Lean.Parser.Tactic.Conv.enter] def evalEnter : Tactic := fun stx => do
@ -334,8 +338,8 @@ private def ext (userName? : Option Name) : TacticM Unit := do
-- show state up to (incl.) next `,` and show errors on `enterArg`
withTacticInfoContext (mkNullNode #[enterArg, sep]) <| withRef enterArg do
match enterArg with
| `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic (← `(conv| arg $arg))
| `(Parser.Tactic.Conv.enterArg| $id:ident) => evalTactic (← `(conv| ext $id))
| `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic (← `(conv| arg $arg))
| `(Parser.Tactic.Conv.enterArg| $id:binderIdent) => evalTactic (← `(conv| ext $id))
| _ => pure ()
end Lean.Elab.Tactic.Conv