## Stream: general

### Topic: constructing expr.lam

#### Scott Morrison (Sep 09 2018 at 08:28):

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 (Sep 09 2018 at 08:29):

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

#### Simon Hudon (Sep 09 2018 at 08:31):

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 (Sep 09 2018 at 08:33):

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 (Sep 09 2018 at 08:55):

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 (Sep 09 2018 at 08:57):

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


Thanks!

#### Simon Hudon (Sep 09 2018 at 09:06):

:+1:

Last updated: May 13 2021 at 06:15 UTC