git.iko.soy/Idris-dev
on master help sign in
Minor, minor readability improvement to Fin.idr
commitb04d0cbcf211943ad07b33ec01debf4e311e5a98 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 16 Mar 2015, 14:10 (12 years ago) parentc666166
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