idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #86 from andylokandy/just

Browse Source 
Add a total version of the fromMaybe
This commit is contained in:
Edwin Brady 2020-05-20 21:41:35 +01:00 committed by GitHub
commit 215ad99308
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/base/Data/Maybe.idr
View File

@ -32,6 +32,12 @@ fromMaybe : (Lazy a) -> Maybe a -> a
fromMaybe def Nothing = def
fromMaybe def (Just j) = j
||| Returns the `a` value of a `Maybe a` which is proved `Just`.
public export
fromJust : (v : Maybe a) -> IsJust v => a
fromJust (Just x) = x
fromJust Nothing impossible
||| Returns `Just` the given value if the conditional is `True`
||| and `Nothing` if the conditional is `False`.
public export