diff options
Diffstat (limited to 'src/Inky/Term/Pretty')
| -rw-r--r-- | src/Inky/Term/Pretty/Error.idr | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr index 651d208..a5ee2fa 100644 --- a/src/Inky/Term/Pretty/Error.idr +++ b/src/Inky/Term/Pretty/Error.idr @@ -73,6 +73,10 @@ prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) = (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) :: prettyNotChecks contra2 prettyNotSynths (LetNS1 contra) = prettyNotSynths contra +prettyNotSynths (LetNS2' (This contra)) = prettyNotSynths contra +prettyNotSynths (LetNS2' (That contra)) = prettyNotSynths contra +prettyNotSynths (LetNS2' (Both contra1 contra2)) = + prettyNotSynths contra1 ++ prettyNotSynths contra2 prettyNotSynths (LetNS2 prf contra) = case synthsRecompute prf of Val a => prettyNotSynths contra @@ -130,6 +134,11 @@ prettyNotChecks (EmbedNC2 _ prf contra) = prettyType b Open )] prettyNotChecks (LetNC1 contra) = prettyNotSynths contra +prettyNotChecks (LetNC2' (This contra)) = prettyNotSynths contra +prettyNotChecks (LetNC2' (That contra)) = prettyNotChecks contra +prettyNotChecks (LetNC2' (Both contra1 contra2)) = + prettyNotSynths contra1 ++ + prettyNotChecks contra2 prettyNotChecks (LetNC2 prf contra) = case synthsRecompute prf of Val _ => prettyNotChecks contra |