Where is this shorthand for match documented?

Stream: new members

[Eduardo Ochs]

Hi all... I was reading the section "Matching on Syntax" of the chapter on syntax of the Metaprogramming book and I stumbled on this,

def isAdd11 : Syntax → Bool
  | `(Nat.add 1 1) => true
  | _ => false

that has a shorthand for match/with that was new to me. Here are two ways to expand it:

inductive N where
  | z         : N
  | s (n : N) : N

def foo1 : N → Bool
  | N.z   => true
  | N.s _ => false

def foo2 : N → Bool := (match · with
  | N.z   => true
  | N.s _ => false)

def foo3 (n : N) : Bool := match n with
  | N.z   => true
  | N.s _ => false

Questions:

1) Is it mentioned in the docs? Where?

2) I couldn't find a way to convert foo1 to a single line by replacing its newlines by semicolons and curly braces. How do I do that?

3) Where is that abbreviation defined in the source? My best guess is that its definition uses matchExprAlt indirectly...

[Damiano Testa]

2. just remove the line breaks: def foo1 : N → Bool | N.z => true | N.s _ => false.

I do not know where this is documented/defined.

[Chris Bailey]

1. It's demonstrated in TPIL here, I don't know if it's explicitly mentioned. TPIL is one of the branches of the manual (the manual links to it near the beginning).

2. It should be part of the command/declar syntax, I think it's the last part of this: https://github.com/leanprover/lean4/blob/239ade80dc6258f68b7ea92e52ef15066f58a791/src/Lean/Parser/Command.lean#L99C5-L99C16

[Eduardo Ochs]

Thanks, @Damiano Testa! I thought that I had tested that, but I hadn't... sorry!

[Eduardo Ochs]

@Chris Bailey, perfect! Many thanks! =)

/-- `declVal` matches the right-hand side of a declaration, one of:
* `:= expr` (a "simple declaration")
* a sequence of `| pat => expr` (a declaration by equations), shorthand for a `match`
* `where` and then a sequence of `field := value` initializers, shorthand for a structure constructor
-/