git.iko.soy/Idris-dev
on master help sign in
Elements of Fin when converted to Nat are smaller than the Bound. (#3407)
9dd3e00Apostolis Xekoukoulotakis
libs/contrib/Data/Fin/Extra.idrnew file+9
compare with master
unifiedsplit
@@ -0,0 +1,9 @@
1+module Data.Fin.Extra
2+
3+import Data.Fin
4+
5+||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
6+public export
7+elemSmallerThanBound : (n : Fin m) -> LTE (finToNat n) m
8+elemSmallerThanBound FZ = LTEZero
9+elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
libs/contrib/contrib.ipkg+3−1
@@ -25,4 +25,6 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
25
25
26 Network.Cgi, Network.Socket,
26 Network.Cgi, Network.Socket,
27
27
28− System.Concurrency.Process
28+ System.Concurrency.Process,
29+
30+ Data.Fin.Extra