diff options
Diffstat (limited to 'src/Data/Maybe/Properties.idr')
| -rw-r--r-- | src/Data/Maybe/Properties.idr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr index f00b79f..495256e 100644 --- a/src/Data/Maybe/Properties.idr +++ b/src/Data/Maybe/Properties.idr @@ -4,3 +4,7 @@ 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 |