git.iko.soy/Idris-dev
on master help sign in
Fix type error in name reflection
c9b1759David Raymond Christiansen
libs/prelude/Language/Reflection/Errors.idr+1−1
compare with master
unifiedsplit
@@ -29,7 +29,7 @@ data Err = Msg String
29 | NoTypeDecl TTName
29 | NoTypeDecl TTName
30 | NotInjective TT TT TT
30 | NotInjective TT TT TT
31 | CantResolve TT
31 | CantResolve TT
32− | CantResolveAlts (List String)
32+ | CantResolveAlts (List TTName)
33 | IncompleteTerm TT
33 | IncompleteTerm TT
34 | UniverseError
34 | UniverseError
35 | ProgramLineComment
35 | ProgramLineComment
src/Idris/ElabTerm.hs+1−1
@@ -2600,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =
2600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2601reflectErr (CantResolveAlts ss) =
2601reflectErr (CantResolveAlts ss) =
2602 raw_apply (Var $ reflErrName "CantResolveAlts")
2602 raw_apply (Var $ reflErrName "CantResolveAlts")
2603− [rawList (Var $ (sUN "String")) (map Var ss)]
2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]
2604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2605reflectErr UniverseError = Var $ reflErrName "UniverseError"
2605reflectErr UniverseError = Var $ reflErrName "UniverseError"
2606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
2606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"