binderIdent vs Ident

Stream: lean4

[Patrick Massot]

How to turn an ident into a binderIdent?

[Patrick Massot]

Knowing the definition is syntax binderIdent := ident <|> hole.

[Jannis Limperg]

import Lean

open Lean

def toBinderIdent (i : Ident) : CoreM (TSyntax ``binderIdent) :=
  `(binderIdent| $i:ident)

That is to say, you probably just need to annotate your use site with :ident.

[Patrick Massot]

Thanks! I wasn't able to use the annotation suggestion but the function works fine.

[Kyle Miller]

I don't think there's any reason to run this in a monad, so here's an alternative:

def toBinderIdent (i : Ident) : TSyntax ``binderIdent := Unhygienic.run <|
  withRef i `(binderIdent| $i:ident)

(The withRef is to tag the resulting binderIdent with the source position of i. Jannis's could have that too.)

[Patrick Massot]

Thanks!