Merge pull request #4547 from JulianKniephoff/elements-smaller-than-bound
Strengthen `elemSmallerThanBound`
commit713ad66b114506a846c315a64cecfa9a9206bbb2
authorNiklas Larsson <metaniklas@gmail.com>
dateThu 27 Sep 2018, 11:27 (8 years ago)
parentbae730a91039ee
libs/contrib/Data/Fin/Extra.idr+2−2
@@ -4,6 +4,6 @@ import Data.Fin
44
55||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
66public export
7−elemSmallerThanBound : (n : Fin m) -> LTE (finToNat n) m
8−elemSmallerThanBound FZ = LTEZero
7+elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
8+elemSmallerThanBound FZ = LTESucc LTEZero
99elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)