edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
903 stars 58 forks source link

Add total version of the fromMaybe #386

Closed andylokandy closed 3 years ago

andylokandy commented 4 years ago

Add Data.Maybe.fromJust : (v : Maybe a) -> IsJust v => a

I think it worth considering if we can also add fromLeft and fromRight for Either.

Alternative:

Rename fromMaybe to fromMaybe', since we usually prime the partial version of the functions. But this is a breaking change.