from binderIdent to funBinder

Stream: lean4

[Ira Fesefeldt]

I would like to create syntax for a simple big Operation that only transverses from 0 to some natural number n, like so:

open Lean Syntax

def bigMin (n : Nat) (f : Nat → Nat) :=
  match n with
  | 0 => f 0
  | n+1 => min (f n+1) (bigMin n f)

syntax "[min] " binderIdent "∈ {0 ... "term" }, " term : term

macro_rules
  | `(term| [min] $x:binderIdent ∈ {0 ... $n}, $v:term) => do
    let acc ← match x.isIdent with
    | true => `(bigMin $n (fun $x ↦ $v))
    | false => `(bigMin $n (fun _ ↦ $v))
    pure acc

I tried to mimic what I saw elsewhere, but I seem to misunderstand something here. The code errors at x.isIdent and at the application of $x to the function. How do I fix these?

Edit: simplified

[Ira Fesefeldt]

I figure out the isIdent part: I required the raw element underneath.

import Lean.Parser.Term

open Lean Syntax

def bigMin (n : Nat) (f : Nat → Nat) :=
  match n with
  | 0 => f 0
  | n+1 => min (f n+1) (bigMin n f)

syntax "[min] " binderIdent "∈ {0 ... "term" }, " term : term

macro_rules
  | `(term| [min] $x:binderIdent ∈ {0 ... $n}, $v:term) => do
    let ident := x.raw
    match ident.isIdent with
    | true => `(bigMin $n (fun $ident ↦ $v))
    | false => `(bigMin $n (fun _ ↦ $v))

However, I still need to transform ident to a funBinder?

[Ira Fesefeldt]

I guess this works:

import Lean.Parser.Term

open Lean Syntax

def bigMin (n : Nat) (f : Nat → Nat) :=
  match n with
  | 0 => f 0
  | n+1 => min (f n+1) (bigMin n f)

syntax "[min] " binderIdent "∈ {0 ... "term" }, " term : term

macro_rules
  | `(term| [min] $x:ident ∈ {0 ... $n}, $v:term) => `(bigMin $n (fun $x => $v))
  | `(term| [min] $_:hole ∈ {0 ... $n}, $v:term) => `(bigMin $n (fun _ => $v))

example : ([min] n ∈ {0 ... 3}, n) = 0 := by
  simp only [bigMin, Nat.reduceAdd, Nat.zero_add, Nat.min_zero]