From 872fde9d1113396739d5653fd73cf9e57a3f4be3 Mon Sep 17 00:00:00 2001 From: ihor rudynskyi Date: Thu, 14 Nov 2024 20:18:48 +0100 Subject: [PATCH 1/4] refactor Uninhabited implementation for Elem types --- CHANGELOG_NEXT.md | 2 + libs/base/Data/List/Elem.idr | 4 +- libs/base/Data/List1/Elem.idr | 5 +-- libs/base/Data/SnocList/Elem.idr | 4 +- libs/base/Data/Vect/Elem.idr | 4 +- tests/base/data_list003/Elem.idr | 21 ++++++++++ tests/base/data_list003/expected | 1 + tests/base/data_list003/run | 3 ++ tests/base/data_listone001/Elem.idr | 39 +++++++++++++++++++ tests/base/data_listone001/expected | 1 + tests/base/data_listone001/run | 3 ++ .../SL.idr | 0 .../expected | 0 .../{data_snoclist => data_snoclist001}/run | 0 tests/base/data_snoclist002/Elem.idr | 21 ++++++++++ tests/base/data_snoclist002/expected | 1 + tests/base/data_snoclist002/run | 3 ++ tests/base/data_vect002/Elem.idr | 21 ++++++++++ tests/base/data_vect002/expected | 1 + tests/base/data_vect002/run | 3 ++ 20 files changed, 128 insertions(+), 9 deletions(-) create mode 100644 tests/base/data_list003/Elem.idr create mode 100644 tests/base/data_list003/expected create mode 100755 tests/base/data_list003/run create mode 100644 tests/base/data_listone001/Elem.idr create mode 100644 tests/base/data_listone001/expected create mode 100755 tests/base/data_listone001/run rename tests/base/{data_snoclist => data_snoclist001}/SL.idr (100%) rename tests/base/{data_snoclist => data_snoclist001}/expected (100%) rename tests/base/{data_snoclist => data_snoclist001}/run (100%) create mode 100644 tests/base/data_snoclist002/Elem.idr create mode 100644 tests/base/data_snoclist002/expected create mode 100755 tests/base/data_snoclist002/run create mode 100644 tests/base/data_vect002/Elem.idr create mode 100644 tests/base/data_vect002/expected create mode 100755 tests/base/data_vect002/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index e3322e182e..812df311d2 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -227,6 +227,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * Added `Data.IORef.atomically` for the chez backend. +* Refactor `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`. + #### Contrib * `Data.List.Lazy` was moved from `contrib` to `base`. diff --git a/libs/base/Data/List/Elem.idr b/libs/base/Data/List/Elem.idr index fdb87da7d9..eccc53994a 100644 --- a/libs/base/Data/List/Elem.idr +++ b/libs/base/Data/List/Elem.idr @@ -19,11 +19,11 @@ data Elem : a -> List a -> Type where There : Elem x xs -> Elem x (y :: xs) export -Uninhabited (Here = There e) where +Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs} e) where uninhabited Refl impossible export -Uninhabited (There e = Here) where +Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs}) where uninhabited Refl impossible export diff --git a/libs/base/Data/List1/Elem.idr b/libs/base/Data/List1/Elem.idr index 22d2bda35a..2c83ff9498 100644 --- a/libs/base/Data/List1/Elem.idr +++ b/libs/base/Data/List1/Elem.idr @@ -21,11 +21,11 @@ data Elem : a -> List1 a -> Type where There : Elem x xs -> Elem x (y ::: xs) export -Uninhabited (List1.Elem.Here = List1.Elem.There e) where +Uninhabited (List1.Elem.Here {x} {xs} = List1.Elem.There {x = x'} {y} {xs} e) where uninhabited Refl impossible export -Uninhabited (List1.Elem.There e = List1.Elem.Here) where +Uninhabited (List1.Elem.There {x} {y} {xs} e = List1.Elem.Here {x = x'} {xs}) where uninhabited Refl impossible export @@ -84,4 +84,3 @@ export elemMap : (0 f : a -> b) -> List1.Elem.Elem x xs -> List1.Elem.Elem (f x) (map f xs) elemMap f Here = Here elemMap f (There el) = There $ elemMap f el - diff --git a/libs/base/Data/SnocList/Elem.idr b/libs/base/Data/SnocList/Elem.idr index 669d4eb77e..8e9f4f913f 100644 --- a/libs/base/Data/SnocList/Elem.idr +++ b/libs/base/Data/SnocList/Elem.idr @@ -14,11 +14,11 @@ data Elem : a -> SnocList a -> Type where There : {0 x, y : a} -> Elem x sx -> Elem x (sx :< y) export -Uninhabited (Here = There e) where +Uninhabited (Here {x} {sx} = There {x = x'} {y} {sx} e) where uninhabited Refl impossible export -Uninhabited (There e = Here) where +Uninhabited (There {x} {y} {sx} e = Here {x = x'} {sx}) where uninhabited Refl impossible export diff --git a/libs/base/Data/Vect/Elem.idr b/libs/base/Data/Vect/Elem.idr index db766f6c0d..0f604bdea9 100644 --- a/libs/base/Data/Vect/Elem.idr +++ b/libs/base/Data/Vect/Elem.idr @@ -17,11 +17,11 @@ data Elem : a -> Vect k a -> Type where There : (later : Elem x xs) -> Elem x (y::xs) export -Uninhabited (Here = There e) where +Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs} e) where uninhabited Refl impossible export -Uninhabited (There e = Here) where +Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs}) where uninhabited Refl impossible export diff --git a/tests/base/data_list003/Elem.idr b/tests/base/data_list003/Elem.idr new file mode 100644 index 0000000000..7bd1425051 --- /dev/null +++ b/tests/base/data_list003/Elem.idr @@ -0,0 +1,21 @@ +import Data.List +import Data.List.Elem + +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem Here Here = Yes Refl +decHomogeneousElem (There _) Here = No uninhabited +decHomogeneousElem Here (There _) = No uninhabited +decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem Here Here = Yes Refl +decHeterogeneousElem (There _) Here = No uninhabited +decHeterogeneousElem Here (There _) = No uninhabited +decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +main : IO () +main = printLn "OK" diff --git a/tests/base/data_list003/expected b/tests/base/data_list003/expected new file mode 100644 index 0000000000..11e42d0821 --- /dev/null +++ b/tests/base/data_list003/expected @@ -0,0 +1 @@ +"OK" diff --git a/tests/base/data_list003/run b/tests/base/data_list003/run new file mode 100755 index 0000000000..7d59490b19 --- /dev/null +++ b/tests/base/data_list003/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Elem.idr diff --git a/tests/base/data_listone001/Elem.idr b/tests/base/data_listone001/Elem.idr new file mode 100644 index 0000000000..62b6c51515 --- /dev/null +++ b/tests/base/data_listone001/Elem.idr @@ -0,0 +1,39 @@ +import Data.List +import Data.List.Elem +import Data.List1 +import Data.List1.Elem + +decHomogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem x xs) -> Dec (el1 = el2) +decHomogeneousElemList Here Here = Yes Refl +decHomogeneousElemList (There _) Here = No uninhabited +decHomogeneousElemList Here (There _) = No uninhabited +decHomogeneousElemList (There el1') (There el2') = case decHomogeneousElemList el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHeterogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElemList Here Here = Yes Refl +decHeterogeneousElemList (There _) Here = No uninhabited +decHeterogeneousElemList Here (There _) = No uninhabited +decHeterogeneousElemList (There el1') (There el2') = case decHeterogeneousElemList el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHomogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem Here Here = Yes Refl +decHomogeneousElem (There _) Here = No uninhabited +decHomogeneousElem Here (There _) = No uninhabited +decHomogeneousElem (There el1') (There el2') = case decHomogeneousElemList el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHeterogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem Here Here = Yes Refl +decHeterogeneousElem (There _) Here = No uninhabited +decHeterogeneousElem Here (There _) = No uninhabited +decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElemList el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +main : IO () +main = printLn "OK" diff --git a/tests/base/data_listone001/expected b/tests/base/data_listone001/expected new file mode 100644 index 0000000000..11e42d0821 --- /dev/null +++ b/tests/base/data_listone001/expected @@ -0,0 +1 @@ +"OK" diff --git a/tests/base/data_listone001/run b/tests/base/data_listone001/run new file mode 100755 index 0000000000..7d59490b19 --- /dev/null +++ b/tests/base/data_listone001/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Elem.idr diff --git a/tests/base/data_snoclist/SL.idr b/tests/base/data_snoclist001/SL.idr similarity index 100% rename from tests/base/data_snoclist/SL.idr rename to tests/base/data_snoclist001/SL.idr diff --git a/tests/base/data_snoclist/expected b/tests/base/data_snoclist001/expected similarity index 100% rename from tests/base/data_snoclist/expected rename to tests/base/data_snoclist001/expected diff --git a/tests/base/data_snoclist/run b/tests/base/data_snoclist001/run similarity index 100% rename from tests/base/data_snoclist/run rename to tests/base/data_snoclist001/run diff --git a/tests/base/data_snoclist002/Elem.idr b/tests/base/data_snoclist002/Elem.idr new file mode 100644 index 0000000000..b95fcb6745 --- /dev/null +++ b/tests/base/data_snoclist002/Elem.idr @@ -0,0 +1,21 @@ +import Data.SnocList +import Data.SnocList.Elem + +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem Here Here = Yes Refl +decHomogeneousElem (There _) Here = No uninhabited +decHomogeneousElem Here (There _) = No uninhabited +decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem Here Here = Yes Refl +decHeterogeneousElem (There _) Here = No uninhabited +decHeterogeneousElem Here (There _) = No uninhabited +decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +main : IO () +main = printLn "OK" diff --git a/tests/base/data_snoclist002/expected b/tests/base/data_snoclist002/expected new file mode 100644 index 0000000000..11e42d0821 --- /dev/null +++ b/tests/base/data_snoclist002/expected @@ -0,0 +1 @@ +"OK" diff --git a/tests/base/data_snoclist002/run b/tests/base/data_snoclist002/run new file mode 100755 index 0000000000..7d59490b19 --- /dev/null +++ b/tests/base/data_snoclist002/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Elem.idr diff --git a/tests/base/data_vect002/Elem.idr b/tests/base/data_vect002/Elem.idr new file mode 100644 index 0000000000..17af651ce7 --- /dev/null +++ b/tests/base/data_vect002/Elem.idr @@ -0,0 +1,21 @@ +import Data.Vect +import Data.Vect.Elem + +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem Here Here = Yes Refl +decHomogeneousElem (There _) Here = No uninhabited +decHomogeneousElem Here (There _) = No uninhabited +decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem Here Here = Yes Refl +decHeterogeneousElem (There _) Here = No uninhabited +decHeterogeneousElem Here (There _) = No uninhabited +decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of + Yes Refl => Yes Refl + No contra => No $ \Refl => contra Refl + +main : IO () +main = printLn "OK" diff --git a/tests/base/data_vect002/expected b/tests/base/data_vect002/expected new file mode 100644 index 0000000000..11e42d0821 --- /dev/null +++ b/tests/base/data_vect002/expected @@ -0,0 +1 @@ +"OK" diff --git a/tests/base/data_vect002/run b/tests/base/data_vect002/run new file mode 100755 index 0000000000..7d59490b19 --- /dev/null +++ b/tests/base/data_vect002/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Elem.idr From 1c82b4b6d9b4b45a403bd178caeec803ebed75de Mon Sep 17 00:00:00 2001 From: ihor rudynskyi Date: Mon, 18 Nov 2024 19:14:15 +0100 Subject: [PATCH 2/4] add different xs --- libs/base/Data/List/Elem.idr | 4 ++-- libs/base/Data/List1/Elem.idr | 4 ++-- libs/base/Data/SnocList/Elem.idr | 4 ++-- libs/base/Data/Vect/Elem.idr | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/libs/base/Data/List/Elem.idr b/libs/base/Data/List/Elem.idr index eccc53994a..46f8484a6a 100644 --- a/libs/base/Data/List/Elem.idr +++ b/libs/base/Data/List/Elem.idr @@ -19,11 +19,11 @@ data Elem : a -> List a -> Type where There : Elem x xs -> Elem x (y :: xs) export -Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs} e) where +Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where uninhabited Refl impossible export -Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs}) where +Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where uninhabited Refl impossible export diff --git a/libs/base/Data/List1/Elem.idr b/libs/base/Data/List1/Elem.idr index 2c83ff9498..775cdcb515 100644 --- a/libs/base/Data/List1/Elem.idr +++ b/libs/base/Data/List1/Elem.idr @@ -21,11 +21,11 @@ data Elem : a -> List1 a -> Type where There : Elem x xs -> Elem x (y ::: xs) export -Uninhabited (List1.Elem.Here {x} {xs} = List1.Elem.There {x = x'} {y} {xs} e) where +Uninhabited (List1.Elem.Here {x} {xs} = List1.Elem.There {x = x'} {y} {xs = xs'} e) where uninhabited Refl impossible export -Uninhabited (List1.Elem.There {x} {y} {xs} e = List1.Elem.Here {x = x'} {xs}) where +Uninhabited (List1.Elem.There {x} {y} {xs} e = List1.Elem.Here {x = x'} {xs = xs'}) where uninhabited Refl impossible export diff --git a/libs/base/Data/SnocList/Elem.idr b/libs/base/Data/SnocList/Elem.idr index 8e9f4f913f..ad8f874e1a 100644 --- a/libs/base/Data/SnocList/Elem.idr +++ b/libs/base/Data/SnocList/Elem.idr @@ -14,11 +14,11 @@ data Elem : a -> SnocList a -> Type where There : {0 x, y : a} -> Elem x sx -> Elem x (sx :< y) export -Uninhabited (Here {x} {sx} = There {x = x'} {y} {sx} e) where +Uninhabited (Here {x} {sx} = There {x = x'} {y} {sx = sx'} e) where uninhabited Refl impossible export -Uninhabited (There {x} {y} {sx} e = Here {x = x'} {sx}) where +Uninhabited (There {x} {y} {sx} e = Here {x = x'} {sx = sx'}) where uninhabited Refl impossible export diff --git a/libs/base/Data/Vect/Elem.idr b/libs/base/Data/Vect/Elem.idr index 0f604bdea9..c4695460a0 100644 --- a/libs/base/Data/Vect/Elem.idr +++ b/libs/base/Data/Vect/Elem.idr @@ -17,11 +17,11 @@ data Elem : a -> Vect k a -> Type where There : (later : Elem x xs) -> Elem x (y::xs) export -Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs} e) where +Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where uninhabited Refl impossible export -Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs}) where +Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where uninhabited Refl impossible export From d33446b1f1963c828526daaa768dfc8b4af34183 Mon Sep 17 00:00:00 2001 From: ihor rudynskyi Date: Wed, 27 Nov 2024 19:25:54 +0100 Subject: [PATCH 3/4] review fixes --- CHANGELOG_NEXT.md | 3 ++- tests/base/data_list003/Elem.idr | 4 ++-- tests/base/data_listone001/Elem.idr | 8 ++++---- tests/base/data_snoclist002/Elem.idr | 4 ++-- tests/base/data_vect002/Elem.idr | 4 ++-- 5 files changed, 12 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 812df311d2..e26c182468 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -227,7 +227,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * Added `Data.IORef.atomically` for the chez backend. -* Refactor `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`. +* Refactor `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem` + so it can be used for homogeneous (===) and heterogeneous (~=~) equality. #### Contrib diff --git a/tests/base/data_list003/Elem.idr b/tests/base/data_list003/Elem.idr index 7bd1425051..05117e767f 100644 --- a/tests/base/data_list003/Elem.idr +++ b/tests/base/data_list003/Elem.idr @@ -1,7 +1,7 @@ import Data.List import Data.List.Elem -decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2) decHomogeneousElem Here Here = Yes Refl decHomogeneousElem (There _) Here = No uninhabited decHomogeneousElem Here (There _) = No uninhabited @@ -9,7 +9,7 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited decHeterogeneousElem Here (There _) = No uninhabited diff --git a/tests/base/data_listone001/Elem.idr b/tests/base/data_listone001/Elem.idr index 62b6c51515..be4550e10d 100644 --- a/tests/base/data_listone001/Elem.idr +++ b/tests/base/data_listone001/Elem.idr @@ -3,7 +3,7 @@ import Data.List.Elem import Data.List1 import Data.List1.Elem -decHomogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem x xs) -> Dec (el1 = el2) +decHomogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem x xs) -> Dec (el1 === el2) decHomogeneousElemList Here Here = Yes Refl decHomogeneousElemList (There _) Here = No uninhabited decHomogeneousElemList Here (There _) = No uninhabited @@ -11,7 +11,7 @@ decHomogeneousElemList (There el1') (There el2') = case decHomogeneousElemList e Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHeterogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElemList Here Here = Yes Refl decHeterogeneousElemList (There _) Here = No uninhabited decHeterogeneousElemList Here (There _) = No uninhabited @@ -19,7 +19,7 @@ decHeterogeneousElemList (There el1') (There el2') = case decHeterogeneousElemLi Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHomogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 === el2) decHomogeneousElem Here Here = Yes Refl decHomogeneousElem (There _) Here = No uninhabited decHomogeneousElem Here (There _) = No uninhabited @@ -27,7 +27,7 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElemList el1' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHeterogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited decHeterogeneousElem Here (There _) = No uninhabited diff --git a/tests/base/data_snoclist002/Elem.idr b/tests/base/data_snoclist002/Elem.idr index b95fcb6745..437baf5964 100644 --- a/tests/base/data_snoclist002/Elem.idr +++ b/tests/base/data_snoclist002/Elem.idr @@ -1,7 +1,7 @@ import Data.SnocList import Data.SnocList.Elem -decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2) decHomogeneousElem Here Here = Yes Refl decHomogeneousElem (There _) Here = No uninhabited decHomogeneousElem Here (There _) = No uninhabited @@ -9,7 +9,7 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited decHeterogeneousElem Here (There _) = No uninhabited diff --git a/tests/base/data_vect002/Elem.idr b/tests/base/data_vect002/Elem.idr index 17af651ce7..6f09d8805c 100644 --- a/tests/base/data_vect002/Elem.idr +++ b/tests/base/data_vect002/Elem.idr @@ -1,7 +1,7 @@ import Data.Vect import Data.Vect.Elem -decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2) decHomogeneousElem Here Here = Yes Refl decHomogeneousElem (There _) Here = No uninhabited decHomogeneousElem Here (There _) = No uninhabited @@ -9,7 +9,7 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl -decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited decHeterogeneousElem Here (There _) = No uninhabited From ca395080f8d08c8e6b185535414df7ba75d17f2b Mon Sep 17 00:00:00 2001 From: ihor rudynskyi Date: Wed, 27 Nov 2024 19:35:07 +0100 Subject: [PATCH 4/4] review fixes --- tests/base/data_list003/Elem.idr | 6 ++++++ tests/base/data_listone001/Elem.idr | 6 ++++++ tests/base/data_snoclist002/Elem.idr | 6 ++++++ tests/base/data_vect002/Elem.idr | 6 ++++++ 4 files changed, 24 insertions(+) diff --git a/tests/base/data_list003/Elem.idr b/tests/base/data_list003/Elem.idr index 05117e767f..f633574c6b 100644 --- a/tests/base/data_list003/Elem.idr +++ b/tests/base/data_list003/Elem.idr @@ -9,6 +9,9 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem' = decHomogeneousElem + decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited @@ -17,5 +20,8 @@ decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem' = decHeterogeneousElem + main : IO () main = printLn "OK" diff --git a/tests/base/data_listone001/Elem.idr b/tests/base/data_listone001/Elem.idr index be4550e10d..e40677b906 100644 --- a/tests/base/data_listone001/Elem.idr +++ b/tests/base/data_listone001/Elem.idr @@ -27,6 +27,9 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElemList el1' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHomogeneousElem' : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem' = decHomogeneousElem + decHeterogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited @@ -35,5 +38,8 @@ decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElemList e Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHeterogeneousElem' : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem' = decHeterogeneousElem + main : IO () main = printLn "OK" diff --git a/tests/base/data_snoclist002/Elem.idr b/tests/base/data_snoclist002/Elem.idr index 437baf5964..66e8f98b0d 100644 --- a/tests/base/data_snoclist002/Elem.idr +++ b/tests/base/data_snoclist002/Elem.idr @@ -9,6 +9,9 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem' = decHomogeneousElem + decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited @@ -17,5 +20,8 @@ decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem' = decHeterogeneousElem + main : IO () main = printLn "OK" diff --git a/tests/base/data_vect002/Elem.idr b/tests/base/data_vect002/Elem.idr index 6f09d8805c..94c2db445e 100644 --- a/tests/base/data_vect002/Elem.idr +++ b/tests/base/data_vect002/Elem.idr @@ -9,6 +9,9 @@ decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2) +decHomogeneousElem' = decHomogeneousElem + decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2) decHeterogeneousElem Here Here = Yes Refl decHeterogeneousElem (There _) Here = No uninhabited @@ -17,5 +20,8 @@ decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' Yes Refl => Yes Refl No contra => No $ \Refl => contra Refl +decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2) +decHeterogeneousElem' = decHeterogeneousElem + main : IO () main = printLn "OK"