module FunErrTest import Language.Reflection import Language.Reflection.Errors import Language.Reflection.Utils %language ErrorReflection total cadr : (xs : List a) -> {auto cons1 : isCons xs = True} -> {auto cons2 : isCons (tail xs) = True} -> a cadr (x :: (y :: _)) {cons1=Refl} {cons2=Refl} = y cadr (x :: []) {cons1=Refl} {cons2=Refl} impossible cadr [] {cons1=Refl} {cons2=Refl} impossible extractList : TT -> Maybe TT extractList (App (App reflCon (App isCons lst)) _) = Just lst extractList _ = Nothing total has2elts : Err -> Maybe (List ErrorReportPart) has2elts (CantSolveGoal tm _) = do lst <- extractList tm return [ TextPart "Could not prove that" , TermPart lst , TextPart "has at least two elements." ] has2elts e = Just [TextPart (show e)] %error_handlers cadr cons1 has2elts %error_handlers cadr cons2 has2elts badCadr1 : Int badCadr1 = cadr [] badCadr2 : Int badCadr2 = cadr [1] goodCadr : Int goodCadr = cadr [1, 2]