Custom binder

Stream: metaprogramming / tactics

[Patrick Johnson]

How to create a syntax rule so that F (a ∈ b), ψ translates to f b (λ a => ψ) where a appears free in ψ?

import Lean
open Lean Elab Term

axiom α : Type
axiom X : α
axiom f : α → (α → α) → α

#check F (a ∈ X), a

And it would be nice if there can be multiple binder parameters, for example:

F (x y ∈ A) (z ∈ B), ψ

should translate to

f A (λ x => f A (λ y => f B (λ z => ψ)))

[Patrick Johnson]

I tried using explicitBinders like in the definition of ∃, but couldn't make it work.

[Ramon Fernandez Mir]

Maybe this trick does what you want?

macro "F (" a:explicitBinders "∈" b:term ")," φ:term : term => do
  let v ← expandExplicitBinders ``id a φ
  `(f $b $v)

#check F (a ∈ X), a -- f X (id fun a => a) : α