Elaborator priority

Stream: lean4

[Patrick Massot]

In

import Lean

open Lean Meta Elab
elab "foo%" t:term : term => do
  let e ← Term.elabTerm t none
  mkAppM `id #[e]

variable (F : Nat → Nat)
#check foo% F 3 -- id (F 3) : Nat

-- how to make it like
#check (id F) 3

How do I avoid foo% consuming all of F 3? The usual algorithm of sticking random precedence numbers in random places didn’t work.

[Aaron Liu]

import Lean

open Lean Meta Elab
elab:max "foo%" t:term:max : term => do
  let e ← Term.elabTerm t none
  mkAppM `id #[e]

variable (F : Nat → Nat)
#check foo% F 3 -- id F 3 : Nat

[Aaron Liu]

I stuck random precedence numbers in random places and it worked lol

[Aaron Liu]

what did you try?

[Patrick Massot]

Thanks Aaron, I forgot that random place!

[Aaron Liu]

I'm Aaron not Aron :)

[Eric Wieser]

That should maybe be elab:max "foo%" t:term:arg

[Patrick Massot]

Sorry about the typo.

[Aaron Liu]

Eric Wieser said:

That should maybe be elab:max "foo%" t:term:arg

What's the difference

[Aaron Liu]

oh it doesn't take do