From 5d0d08162e1dffa019c629e2ee4f776310942c85 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Mon, 25 Sep 2023 13:12:22 +0100 Subject: [PATCH] [ compat ] base now has quantity 0 for cong's argument (#33) --- src/Core/Case/Builder.idr | 2 +- src/Core/TT/Name.idr | 2 +- src/Core/TT/TT.idr | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Core/Case/Builder.idr b/src/Core/Case/Builder.idr index f1993632..d3c506e9 100644 --- a/src/Core/Case/Builder.idr +++ b/src/Core/Case/Builder.idr @@ -459,7 +459,7 @@ conTypeEq (CName x tag) (CName x' tag') Yes Refl => Just Refl No contra => Nothing conTypeEq CDelay CDelay = Just Refl -conTypeEq (CConst x) (CConst y) = cong CConst <$> constantEq x y +conTypeEq (CConst x) (CConst y) = (\ eq => cong CConst eq) <$> constantEq x y conTypeEq _ _ = Nothing data Group : SnocList Name -> -- variables in scope diff --git a/src/Core/TT/Name.idr b/src/Core/TT/Name.idr index 1060f689..c1fe1f45 100644 --- a/src/Core/TT/Name.idr +++ b/src/Core/TT/Name.idr @@ -387,7 +387,7 @@ nameEq (NS xs x) (NS ys y) with (decEq xs ys) nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl nameEq (NS xs x) (NS ys y) | (No contra) = Nothing -nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y) +nameEq (UN x) (UN y) = map (\ eq => cong UN eq) (userNameEq x y) nameEq (MN x t) (MN x' t') with (decEq x x') nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t') nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl diff --git a/src/Core/TT/TT.idr b/src/Core/TT/TT.idr index b2e891ff..d46cd21c 100644 --- a/src/Core/TT/TT.idr +++ b/src/Core/TT/TT.idr @@ -153,7 +153,7 @@ constantEq (Ch x) (Ch y) = case decEq x y of Yes Refl => Just Refl No contra => Nothing constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles! -constantEq (PrT x) (PrT y) = cong PrT <$> primTypeEq x y +constantEq (PrT x) (PrT y) = (\ eq => cong PrT eq) <$> primTypeEq x y constantEq WorldVal WorldVal = Just Refl constantEq _ _ = Nothing