pfun to total function

Stream: Is there code for X?

[Bernd Losert]

I don't see a function that takes an f : α →. β and gives me back f.dom → β. The closest seems to be pfun.fn. Or am I not looking hard enough?

[Eric Wieser]

What type is docs#pfun.dom?

[Eric Wieser]

You're looking for docs#pfun.as_subtype

[Eric Wieser]

Did you try library_search?

[Bernd Losert]

Ah, that's what it's called. No, I didn't try library_search for this.

[Bernd Losert]

Hmm... is there an equivalent to pfun but for option? data.pfun has a lot of functions that I need, but I need option versions.

[Eric Wieser]

Can you write your question as a #mwe? If you do, then library_search might be able to answer it

[Bernd Losert]

For example,

example (f : α → option β) : {x : α | is_some (f x)} → β := by library_search

[Bernd Losert]

Hmm... I realize that I need to talk about "nondegenerate" α → option β functions, i.e. there is at least one value that produces a some.

[Eric Wieser]

That seems less likely to exist (and maybe less worthwhile to have in mathlib), but should be trivial to define for your own use

[Eric Wieser]

Something like λ a, (f a).get (f a).prop