idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 19:13:02 +03:00
Code Issues Projects Releases Wiki Activity

Add Control.Validation module to contrib package.

Browse Source
This commit is contained in:
Sventimir 2020-08-12 17:33:25 +02:00
parent f3168d16aa
commit 67bab6b088
2 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libs/base/Data/Nat.idr
View File

@ -58,6 +58,7 @@ data NotBothZero : (n, m : Nat) -> Type where
LeftIsNotZero : NotBothZero (S n) m
RightIsNotZero : NotBothZero n (S m)
export
Uninhabited (NotBothZero 0 0) where
uninhabited LeftIsNotZero impossible
uninhabited RightIsNotZero impossible

2
libs/contrib/contrib.ipkg
View File

@ -12,6 +12,8 @@ modules = Control.ANSI,
Control.Algebra.Laws,
Control.Algebra.Implementations,
Control.Validation,
Data.Bool.Algebra,
Data.Linear.Array,