## 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?

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: May 11 2021 at 22:14 UTC