blob: 495256e443efc60a21eb2d990d1822baf9563971 (
plain)
1
2
3
4
5
6
7
8
9
10
|
module Data.Maybe.Properties
export
mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
mapFusion Nothing = Refl
mapFusion (Just x) = Refl
export
appNothingRight : (0 f : a -> b) -> (y : Maybe a) -> Just f <*> y = Nothing -> y = Nothing
appNothingRight f Nothing prf = Refl
|
