codomain of expr

Stream: general

[Chris Hughes]

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]

That must be meta, right?

[Chris Hughes]

Yes

[Floris van Doorn]

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

[Floris van Doorn]

Or more directly:

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

[Keeley Hoek]

Be weary that the result will contain vars

[Simon Hudon]

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.