From f3f00451c85ac96d5c64d63c29164bbada2a80bc Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 30 Nov 2024 04:12:53 -0800 Subject: [PATCH] feat: add `structInstFieldDecl` syntax category (#6265) This PR is preparation for changes to structure instance notation in #6165. It adds a syntax category that will be used for field syntax. --- src/Init/Notation.lean | 5 +++++ src/Lean/Parser/Term.lean | 7 +++++++ 2 files changed, 12 insertions(+) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 80ce48bd2482..402b762cb995 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -48,6 +48,11 @@ def tactic : Category := {} For example, `let x ← e` is a `doElem`, and a `do` block consists of a list of `doElem`s. -/ def doElem : Category := {} +/-- `structInstFieldDecl` is the syntax category for value declarations for fields in structure instance notation. +For example, the `:= 1` and `where a := 3` in `{ x := 1, y where a := 3 }` are in the `structInstFieldDecl` class. +This category is necessary because structure instance notation is recursive due to the `x where ...` field notation. -/ +def structInstFieldDecl : Category := {} + /-- `level` is a builtin syntax category for universe levels. This is the `u` in `Sort u`: it can contain `max` and `imax`, addition with constants, and variables. -/ diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 66b9a4d5d27f..8cf659a87420 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -387,6 +387,13 @@ use `(_)` to inhibit this and have it be solved for by unification instead, like explicitBinder requireType <|> strictImplicitBinder requireType <|> implicitBinder requireType <|> instBinder +/- +Syntax category for structure instance notation fields. +Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible. +-/ +builtin_initialize + registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl + /- It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case. `{α} → α → α` would be short for `{α : Type} → α → α`