1
0
forked from GitHub/gf-rgl

Maybe.gf: add isJust function (synonym for exists)

This commit is contained in:
john.j.camilleri
2014-01-29 11:17:50 +00:00
parent e249ae54d1
commit 8c978b3e1d

View File

@@ -26,6 +26,7 @@ resource Maybe = open Prelude, Predef in {
-- Functions
exists : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;
isJust : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;
fromJust : (T : Type) -> Maybe T -> T = \_,m -> case m.exists of {
True => m.inner ;
False => Predef.error "Called fromJust with Nothing"