>>> fromJust (Just 1) 1
>>> 2 * (fromJust (Just 10)) 20
>>> 2 * (fromJust Nothing) *** Exception: Maybe.fromJust: Nothing ...WARNING: This function is partial. You can use case-matching instead.
>>> fromJust (sJust (literal 'a')) 'a' :: SChar >>> prove $ \x -> fromJust (sJust x) .== (x :: SChar) Q.E.D. >>> sat $ \x -> x .== (fromJust sNothing :: SChar) Satisfiable. Model: s0 = 'A' :: CharNote how we get a satisfying assignment in the last case: The behavior is unspecified, thus the SMT solver picks whatever satisfies the constraints, if there is one.