Zulip Chat Archive

Stream: general

Topic: constructing expr.lam


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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,

view this post on Zulip Scott Morrison (Sep 09 2018 at 09:06):

Thanks!

view this post on Zulip Simon Hudon (Sep 09 2018 at 09:06):

:+1:


Last updated: May 13 2021 at 06:15 UTC