constructing expr.lam

Stream: general

[Scott Morrison]

How do I construct expr.lam terms? In particular, I have an expression e_1 that already has a var n inside it, and another e_2, and I want to construct the expr representing lam x, e_1 = e_2.

[Scott Morrison]

I tried to use to_expr ``(%%e_1 = %%e_2), but that chokes because e_1 has a var inside it.

[Simon Hudon]

It's kind of ugly but I recommend

feq <- mk_const `eq,
v <- mk_mvar,
let e := lam n bi t (feq v e_1 e_2)

[Simon Hudon]

the downside is that you're postponing type checking. If you don't want to postpone type checking, you have to take the long way around, instantiate your var with local_const, type check, then use lambdas

[Scott Morrison]

Ah, I see. Turning my var into a local_const is maybe not so bad, in any case. How does one construct the expr.lam then?

[Simon Hudon]

v <- mk_local_def n t,
e <- mk_app `eq [e_1.instantiate_var v, e_2],
lambdas [v] e,

[Scott Morrison]

Thanks!

[Simon Hudon]

:+1: