Is there a dependent partial function type in mathlib4?

Stream: new members

[nemo]

I found the independent partial function type PFun in mathlib4, but to my surprise, then failed to find a dependent one. And it seems easy to define (x : \alpha) \to. \beta x to be (x : \alpha) \to Part (\beta x). Is it unnecessary to define it, or is it just to be done?

[Aaron Liu]

I guess no one has needed it yet

[Weiyi Wang]

Does thia definition allow one to write a function where \beta sometimes can't output a type for certain \alpha?

[nemo]

Now I've found it tricky to allow \beta be a Part Type. The problem is \beta x (for x : \alpha) can't be a codomain if it is not garanteed to be a Type

[Kenny Lau]

it was a question, you didn't have to follow it

[nemo]

I find there to be two ways : (1) let \beta xbe Empty if it doesn' exist (2) let \beta x be Unit instead. (1) makes it to be (x : \alpha) \to (h : (\beta x).Dom) \to (\beta x).get h, and (2) makes (x : \alpha) \to. \beta x to be Empty iff \beta is not total

[Robin Arnez]

Hmm I don't feel like \beta being a Part has any purpose

[Robin Arnez]

Like, what should that even mean? Empty? Well then you could also just use Empty directly