mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
13 lines
330 B
Idris
13 lines
330 B
Idris
|
module NestedWith
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
interface DecEq a where
|
||
|
|
decEq : (x, y : a) -> Dec (x === y)
|
||
|
|
|
||
|
|
(DecEq a, DecEq b) => DecEq (a, b) where
|
||
|
|
decEq (x, y) (a, b) with (decEq x a) | (decEq y b)
|
||
|
|
_ | Yes eqL | Yes eqR = Yes (cong2 (,) eqL eqR)
|
||
|
|
_ | No neqL | _ = No (neqL . cong fst)
|
||
|
|
_ | _ | No neqR = No (neqR . cong snd)
|