Define Macro

Stream: lean4

[Joseph O]

in this code

syntax binder' := "(" ident " : " term ")"
syntax "def" ident binder'* " -> " term " : " term : command

macro_rules
  | `(def $f:ident ($a:ident : $ty:term) -> $ty':term: $v:term) =>
    `(def $f:ident -> ($ty:term -> $ty:term): fun $a:ident => $v:term)
  | `(def $f:ident ($a:ident : $ty:term) $bs:binder'* -> $ty':term: $v:term) =>
    `(def $f:ident $bs:binder'* -> ($ty:term -> $ty':term): fun $a => $v:term)

def add (a : Nat) (b : Nat) -> Nat:
  x + y

Im getting the error elaboration function for '«commandDef___->_:_»' has not been implemented for the add function. Any ideas why?

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

Hm i wonder why this has errors

syntax binder' := ident term
syntax "sub" ident "(" sepBy(binder', ",") ")" " returns " term "{" term "}" : command

macro_rules
  | `(sub $f:ident ($a:ident $ty:term) returns ty':term { $v:term }) =>
    `(def $f:ident : ($ty:term -> $ty':term) := fun $a:ident => $v:term)
  | `(sub $f:ident ($bs:binder',* $a:ident $ty:term) returns $ty':term { $v:term }) =>
    `(sub $f:ident ($bs:binder',*) returns ($ty:term -> $ty':term) { fun $a:ident => $v:term })

[Joseph O]

here are the errors:

expected '{'

elaboration function for 'antiquot' has not been implemented
  $ty:term

expected command

expected ')'

expected '}' or identifier

[Joseph O]

Shouldnt this work the same as the first one?

[Joseph O]

Im a bit confused

[Joseph O]

Unless I translated incorrectly

[Sebastian Ullrich]

At around the location of the first error there is a clear mistake, a typo basically. Try double-checking that part.

[Joseph O]

Sebastian Ullrich said:

At around the location of the first error there is a clear mistake, a typo basically. Try double-checking that part.

Ok I fixed it and now I have these errors

expected 'ident', '}' or identifier

elaboration function for 'antiquot' has not been implemented
  $ty:term

expected command

expected ')'

expected '}' or identifier

[Siddharth Bhat]

I believe you're having trouble because { .. } is consumed by the term parser, since we can build records using {..} syntax.

For example, this minimal program produces a similar error:

syntax "returns" term "{" term "}" : command

macro_rules
| `(returns $x:term { $y:term  }) => `("foo")
-- expected 'ident', '}' or identifier

On the other hand, something like this where we add a clear delineation between term and { succeeds:

syntax "returns" term ";;" "{" term "}" : command
-- New: `;;` in the rule.
macro_rules
| `(returns $x:term ;; { $y:term  }) => `("foo")

[Siddharth Bhat]

(DELETED: editing snafu)

[Joseph O]

Siddharth Bhat said:

I believe you're having trouble because { .. } is consumed by the term parser, since we can build records using {..} syntax.

For example, this minimal program produces a similar error:

syntax "returns" term "{" term "}" : command

macro_rules
| `(returns $x:term { $y:term  }) => `("foo")
-- expected 'ident', '}' or identifier

On the other hand, something like this where we add a clear delineation between term and { succeeds:

syntax "returns" term ";;" "{" term "}" : command
-- New: `;;` in the rule.
macro_rules
| `(returns $x:term ;; { $y:term  }) => `("foo")

So there is no way we can avoid that?