From db43de7b9d4c5059ea4a5db87a347387f3983629 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 23 Aug 2025 10:16:53 -0700 Subject: [PATCH] feat: add `enter [in patt]` syntax (#10081) This PR adds `enter [in patt]` syntax. The implementation will come in a followup PR, and it will stand for `pattern patt`. --- src/Init/Conv.lean | 6 +++++- stage0/src/stdlib_flags.h | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 017ee55b64..55c24a1073 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -290,13 +290,17 @@ macro "right" : conv => `(conv| rhs) /-- `intro` traverses into binders. Synonym for `ext`. -/ macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*) -syntax enterArg := binderIdent <|> argArg +syntax enterPattern := "in " (occs)? term + +syntax enterArg := binderIdent <|> argArg <|> enterPattern /-- `enter [arg, ...]` is a compact way to describe a path to a subterm. It is a shorthand for other conv tactics as follows: * `enter [i]` is equivalent to `arg i`. * `enter [@i]` is equivalent to `arg @i`. * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`. +* `enter [in e]` (where `e` is a term) is equivalent to `pattern e`. + Occurrences can be specified with `enter [in (occs := ...) e]`. For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]` will traverse to the subterm `b`. -/ syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..a6831f9883 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -25,4 +25,4 @@ options get_default_options() { #endif return opts; } -} +}//trigger stage0 update