git.iko.soy/Idris-dev
on master help sign in
Minor, minor readability improvement to Fin.idr
b04d0cbDavid Raymond Christiansen
libs/base/Data/Fin.idr+1−1
compare with master
unifiedsplit
@@ -179,7 +179,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))
179 , TextPart "is less than", TermPart (getNat m)
179 , TextPart "is less than", TermPart (getNat m)
180 , TextPart "because", TermPart (P Bound n t)
180 , TextPart "because", TermPart (P Bound n t)
181 , TextPart "is a bound variable instead of a constant"
181 , TextPart "is a bound variable instead of a constant"
182− , TermPart (TConst (AType (ATInt ITBig)))
182+ , TermPart `(Integer : Type)
183 ]
183 ]
184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
185 = mkFinIntegerErr n m
185 = mkFinIntegerErr n m