Zulip Chat Archive

Stream: general

Topic: codomain of expr


view this post on Zulip Chris Hughes (Aug 02 2019 at 15:07):

Is there an easy way to get the domain of an expr representing a bunch of nested pis? Given A -> B -> C -> D I want to return D

view this post on Zulip Johan Commelin (Aug 02 2019 at 15:10):

That must be meta, right?

view this post on Zulip Chris Hughes (Aug 02 2019 at 15:12):

Yes

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:13):

meta def codomain (e : expr) : expr :=
if e.is_pi then codomain e.binding_body else e

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:14):

Or more directly:

open expr
meta def codomain : expr → expr
| (pi _ _ _ b)  := codomain b
| e             := e

view this post on Zulip Keeley Hoek (Aug 02 2019 at 15:22):

Be weary that the result will contain vars

view this post on Zulip Simon Hudon (Aug 02 2019 at 15:31):

A safer route would be:

(vs,e) <- mk_local_pis e which produces vs a list of variables created to stand for the bound variables of the removed pis and e the codomain that you're looking for.


Last updated: May 11 2021 at 22:14 UTC