Optionally bracketed binder

Stream: lean4

[Horatiu Cheval]

A basic macro question that came up in the new members stream, I'll ask a more appropriate question here. I tried to define a macro for assume from Lean3. I came up with this, which works, but requires brackets in assume (h : p) h.

macro "assume" var:bracketedBinder exp:term : term => `(fun $var => $exp)

How can I make the brackets optional, like they are in fun?

[Horatiu Cheval]

The example might be problematic since it is not clear how to separate p from t in assume h : p t, but suppose I wanted to defined something like \Pi from Lean3 as an alias for \forall, which takes a comma there, so that the separation is clear.

[Mac]

@Horatiu Cheval If you take a look at the definition of fun in the Lean 4 source, you can discover that it uses funBinder instead of bracketedBinder in its parser. Thus, you can do the same like so:

import Lean.Parser.Term
open Lean Parser Term
macro "assume " var:funBinder ", " exp:term : term => `(fun $var => $exp)

[Mac]

However, if you want your macro to more closely mirror standard syntax, you will probably want assume to accept multiple binders like so:

macro "assume" vars:many1(ppSpace funBinder) ", " exp:term : term =>
  `(fun $(vars.getArgs)* => $exp)

def foo : Nat → Nat → Nat := assume x y, 0
#print foo -- def foo : Nat → Nat → Nat := fun x y => 0

[Horatiu Cheval]

That's great, thank you! I noticed that file myself but I couldn't manage to find my way through it