macro problem

Stream: lean4

[Joseph O]

Why doesn't this macro work?

syntax "let" ident "=" term "=>" term : term

macro_rules
  | `(let $name:ident := $v:term in $e:term) =>
    `(let $name := $v; $e)

def test : Nat :=
  let x := 1 in x+1

getting the error expected term

[Sébastien Michelland]

Your syntax rule doesn't match the matching that you perform in macro_rules. There's = vs := and => vs in. Try this:

syntax "let" ident ":=" term "in" term : term

macro_rules
  | `(let $name:ident := $v:term in $e:term) =>
    `(let $name := $v; $e)

def test : Nat :=
  let x := 1 in x+1

#eval test -- 2

[Arthur Paulino]

Or maybe you meant this?

syntax "let" ident "=" term "=>" term : term

macro_rules
  | `(let $name:ident = $v:term => $e:term) =>
    `(let $name := $v; $e)

def test : Nat :=
  let x = 1 => x+1

#eval test -- 2

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

Oh wait how come in this case i get the error expected term

| `(let* $name:ident := $v:term in $t:term) => `(let rec $name := $v; $t)