diff --git a/src/prelude/Maybe.gf b/src/prelude/Maybe.gf index f2ea1bd0..e892958f 100644 --- a/src/prelude/Maybe.gf +++ b/src/prelude/Maybe.gf @@ -9,21 +9,27 @@ resource Maybe = open Prelude, Predef in { -- Constructors Maybe : (t : Type) -> Type = \t -> { inner : t ; - exists : Bool + exists : Bool ; } ; Just : (T : Type) -> T -> Maybe T = \_,t -> { inner = t ; - exists = True + exists = True ; } ; - -- Nothing : (T : Type) -> Maybe T = \_ -> { - -- inner = variants {} ; - -- exists = False - -- } ; Nothing : (T : Type) -> T -> Maybe T = \_,t -> { inner = t ; - exists = False + exists = False ; } ; + -- IMPORTANT + -- This version of Nothing would be preferred, but it may not work as expected. + -- This happens when using Nothing within a record. For discussion of this see: + -- https://groups.google.com/d/msg/gf-dev/KAQEttN-0Cs/EjGHjOXEKO0J + Nothing' : (T : Type) -> Maybe T = \_ -> { + inner = variants {} ; + exists = False ; + } ; + -- You have been warned! + -- Functions exists : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ; isJust : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;