idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Add some Uninhabited implementations

Browse Source
This commit is contained in:
Nick Drozd 2020-06-29 19:55:47 -05:00 committed by G. Allais
parent 7c923944ae
commit faabbfcea1
2 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/base/Data/Fin.idr
View File

@ -21,6 +21,14 @@ implementation Uninhabited (Fin Z) where
uninhabited FZ impossible
uninhabited (FS f) impossible
export
Uninhabited (FZ = FS k) where
uninhabited Refl impossible
export
Uninhabited (FS k = FZ) where
uninhabited Refl impossible
export
FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
FSInjective left _ Refl = Refl

16
libs/prelude/Prelude.idr
View File

@ -70,6 +70,14 @@ infixl 9 `div`, `mod`
public export
data Bool = True | False
public export
Uninhabited (True = False) where
uninhabited Refl impossible
public export
Uninhabited (False = True) where
uninhabited Refl impossible
||| Boolean NOT.
public export
not : (1 b : Bool) -> Bool
@ -811,6 +819,14 @@ data Maybe : (ty : Type) -> Type where
||| A value of type `ty` is stored
Just : (1 x : ty) -> Maybe ty
public export
Uninhabited (Nothing = Just x) where
uninhabited Refl impossible
public export
Uninhabited (Just x = Nothing) where
uninhabited Refl impossible
public export
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing = n