@@ -462,6 +462,7 @@ readFile fn = do h <- openFile fn Read
463%language ErrorReflection
463%language ErrorReflection
465cast_part : TT -> ErrorReportPart
466cast_part : TT -> ErrorReportPart
466cast_part (P Bound n t) = TextPart "unknown type"
467cast_part (P Bound n t) = TextPart "unknown type"
467cast_part x = TermPart x
468cast_part x = TermPart x
@@ -475,3 +476,9 @@ cast_error (CantResolve `(Cast ~x ~y))
475 cast_part y]
476 cast_part y]
476cast_error _ = Nothing
477cast_error _ = Nothing
480+num_error : Err -> Maybe (List ErrorReportPart)
481+num_error (CantResolve `(Num ~x))
482+ = Just [TermPart x, TextPart "is not a numeric type"]
483+num_error _ = Nothing