Zulip Chat Archive

Stream: general

Topic: codomain of expr


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

Johan Commelin (Aug 02 2019 at 15:10):

That must be meta, right?

Chris Hughes (Aug 02 2019 at 15:12):

Yes

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

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

Keeley Hoek (Aug 02 2019 at 15:22):

Be weary that the result will contain vars

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: Dec 20 2023 at 11:08 UTC