Elements of Fin when converted to Nat are smaller than the Bound. (#3407)
commit9dd3e00258345aa9184b3ae5d803d83272226410
authorApostolis Xekoukoulotakis <apostolis.xekoukoulotakis@gmail.com>
dateMon 31 Oct 2016, 22:44 (10 years ago)
parentba82f90
libs/contrib/Data/Fin/Extra.idrnew file+9
@@ -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,
2525
2626 Network.Cgi, Network.Socket,
2727
28− System.Concurrency.Process
28+ System.Concurrency.Process,
29+
30+ Data.Fin.Extra