Remove SFin.

Delete unused modules.

Restructure some proofs to reduce the number of lemmas.

1 files changed, 0 insertions, 92 deletions

diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
deleted file mode 100644
index c9fea96..0000000
--- a/src/Data/Maybe/Properties.idr
+++ /dev/null
@@ -1,92 +0,0 @@
-module Data.Maybe.Properties
-
-import Control.Function
-import Data.Maybe
-
-public export
-data IsNothing : Maybe a -> Type where
-  ItIsNothing : IsNothing Nothing
-
-%inline
-export
-mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
-mapFusion Nothing = Refl
-mapFusion (Just x) = Refl
-
-%inline
-export
-extractIsJust : {x : Maybe a} -> (0 _ : IsJust x) -> (y ** x = Just y)
-extractIsJust ItIsJust = (_ ** Refl)
-
-%inline
-export
-extractIsNothing : {x : Maybe a} -> (0 _ : IsNothing x) -> x = Nothing
-extractIsNothing ItIsNothing = Refl
-
-%inline
-export
-mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
-mapIsJust f ItIsJust = ItIsJust
-
-%inline
-export
-mapJustInverse :
-  (0 f : a -> b) ->
-  (x : Maybe a) ->
-  (0 _ : map f x = Just y) ->
-  (z ** (x = Just z, y = f z))
-mapJustInverse f (Just x) prf = (x ** (Refl, sym $ injective prf))
-
-%inline
-export
-mapNothing : (0 f : a -> b) -> IsNothing x -> IsNothing (map f x)
-mapNothing f ItIsNothing = ItIsNothing
-
-%inline
-export
-mapNothingInverse :
-  (0 f : a -> b) ->
-  (x : Maybe a) ->
-  (0 _ : IsNothing (map f x)) ->
-  IsNothing x
-mapNothingInverse f Nothing prf = ItIsNothing
-
-%inline
-export
-appIsJust : IsJust f -> IsJust x -> IsJust (f <*> x)
-appIsJust ItIsJust ItIsJust = ItIsJust
-
-%inline
-export
-appJustInverse :
-  (f : Maybe (a -> b)) ->
-  (x : Maybe a) ->
-  (0 _ : f <*> x = Just y) ->
-  (f' ** x' ** (f = Just f', x = Just x', y = f' x'))
-appJustInverse (Just f) (Just x) prf = (f ** x ** (Refl, Refl, sym $ injective prf))
-
-%inline
-export
-appLeftNothingIsNothing : IsNothing f -> (0 x : Maybe a) -> IsNothing (f <*> x)
-appLeftNothingIsNothing ItIsNothing x = ItIsNothing
-
-%inline
-export
-appRightNothingIsNothing : (f : Maybe (a -> b)) -> IsNothing x -> IsNothing (f <*> x)
-appRightNothingIsNothing Nothing prf = ItIsNothing
-appRightNothingIsNothing (Just f) ItIsNothing = ItIsNothing
-
-%inline
-export
-appNothingInverse :
-  (f : Maybe (a -> b)) ->
-  (x : Maybe a) ->
-  (0 _ : IsNothing (f <*> x)) ->
-  Either (IsNothing f) (IsNothing x)
-appNothingInverse Nothing x prf = Left ItIsNothing
-appNothingInverse (Just f) Nothing prf = Right ItIsNothing
-
-%inline
-export
-bindNothing : {x : Maybe a} -> (0 ok : IsNothing x) -> (f : a -> Maybe b) -> IsNothing (x >>= f)
-bindNothing ItIsNothing f = ItIsNothing