diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 18:13:22 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 18:13:22 +0000 |
| commit | 865dc549baf613e45e2f79036d54850a483fa509 (patch) | |
| tree | 1638d8bf6544ede436a3d933dcdc2c0faf59727c | |
| parent | 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd (diff) | |
Fix bad annotation when desugaring map.
| -rw-r--r-- | src/Inky/Term/Desugar.idr | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr index 1ce0e41..7051e4b 100644 --- a/src/Inky/Term/Desugar.idr +++ b/src/Inky/Term/Desugar.idr @@ -141,9 +141,9 @@ desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) = Annot meta (Abs meta (["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg")))) - (TArrow (TArrow (TArrow b c) - (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)) - (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)) + (TArrow (TArrow b c) (TArrow + (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a) + (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))) desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1 desugarChecks (VarC prf1 prf2) = desugarSynths prf1 @@ -249,9 +249,9 @@ maybeDesugar (Map meta (x ** a) b c) = Annot meta (Abs meta (["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg")))) - (TArrow (TArrow (TArrow b c) - (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)) - (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)) + (TArrow (TArrow b c) (TArrow + (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a) + (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))) maybeDesugarList [] = pure [] maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |] |