Polimorphic lam Expr

Stream: metaprogramming / tactics

[Bernardo Borges]

Hello Everybody!
I am learning metaprogramming with the book and I am stuck in the MetaM exercises, where I need to create a Expr of for the code:

fun x => 5

But as of my understanding, the way to create a lambda expressions forces us to pass the type, so I am stuck with:

let const5 : Expr := .lam `x (sorry) (mkNatLit 5) BinderInfo.default

Any suggestions?

[Adam Topaz]

I think .const ``Nat [] is what you want for your sorry

[Adam Topaz]

well, depending on what type you want x to have :)

[Bernardo Borges]

Yes, that will work and yield a

fun x => 5 : Nat → Nat

I was thinking there could be a fully polimorphic answer that could yield :

 a -> Nat

[Adam Topaz]

Ah, but in that case a should be another free variable in the function.

[Bernardo Borges]

Oh, and is it possible to combine this free variable with the Expr.lam ? I never used it.

[Kyle Miller]

It'd be a nested lambda, where the first is a BinderInfo.implicit for the argument a whose type is .sort levelOne (or whatever universe you want). You can't define a lambda that's also universe polymorphic.

In Lean syntax, it's fun {a : Type} (x : a) => 5