git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2002 from david-christiansen/better-fin-error

Minor, minor readability improvement to Fin.idr

commit39ba4329041251573cef57e57591ea2c4ca2454b authorDavid Christiansen <david@davidchristiansen.dk> dateMon 16 Mar 2015, 21:46 (12 years ago) parent6d768bbb04d0cb
1 file changed+1−1
compare with master
unifiedsplit
libs/base/Data/Fin.idr+1−1
libs/base/Data/Fin.idr+1−1
@@ -179,7 +179,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))
179179 , TextPart "is less than", TermPart (getNat m)
180180 , TextPart "because", TermPart (P Bound n t)
181181 , TextPart "is a bound variable instead of a constant"
182− , TermPart (TConst (AType (ATInt ITBig)))
182+ , TermPart `(Integer : Type)
183183 ]
184184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
185185 = mkFinIntegerErr n m