@@ -462,6 +462,7 @@ readFile fn = do h <- openFile fn Read
462462
463463%language ErrorReflection
464464
465+private
465466cast_part : TT -> ErrorReportPart
466467cast_part (P Bound n t) = TextPart "unknown type"
467468cast_part x = TermPart x
@@ -475,3 +476,9 @@ cast_error (CantResolve `(Cast ~x ~y))
475476 cast_part y]
476477cast_error _ = Nothing
477478
479+%error_handler
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
484+