Open rutenkolk opened 5 years ago
Hi,
when a typecheck fails, vim-idris prints a less understandable error message than the standard idris repl.
It's the "Specifically" section that get's messed up.
As an example let's take the (wronlgy typed) ++ Function for Vect from the tutorial at
http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html
idris repl prints exactly what is also printed in the tutorial: Specifically: Type mismatch between plus k k and plus k m
Specifically: Type mismatch between plus k k and plus k m
But in vim I get
Specifically: Type mismatch between plus k k and plus k mUnification failure
Is this just a missing newline before "Unification failure"?
Hi,
when a typecheck fails, vim-idris prints a less understandable error message than the standard idris repl.
It's the "Specifically" section that get's messed up.
As an example let's take the (wronlgy typed) ++ Function for Vect from the tutorial at
http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html
idris repl prints exactly what is also printed in the tutorial:
Specifically: Type mismatch between plus k k and plus k mBut in vim I get
Specifically: Type mismatch between plus k k and plus k mUnification failureIs this just a missing newline before "Unification failure"?