diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-06-30 18:34:49 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-06-30 18:34:49 +0100 |
| commit | 621f6221048213dc4d359581197988050af99d0d (patch) | |
| tree | 5e218ed3a641f4079b37b1143d7624f55535e568 /src/Data/Maybe | |
| parent | 9d595c4ad37b58385908dc46b3413aacc4f2e4b7 (diff) | |
Define thinning and thickening.
Diffstat (limited to 'src/Data/Maybe')
| -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 |