Skip to content

Instantly share code, notes, and snippets.

@gallais
Created Jun 4, 2019
Embed
What would you like to do?
Use case for ∷-dec
open import Data.List using (List); open List
open import Data.List.Properties
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
private variable A : Set
data Rose (A : Set) : Set where
node : List (Rose A) Rose A
node-injective : {xs ys : List (Rose A)} node xs ≡ node ys xs ≡ ys
node-injective refl = refl
_≟_ : Decidable {A = Rose A} _≡_
_≟s_ : Decidable {A = List (Rose A)} _≡_
node xs ≟ node ys = map′ (cong node) node-injective (xs ≟s ys)
-- _≟s_ = ≡-dec _≟_ -- termination error
[] ≟s [] = yes refl
[] ≟s (x ∷ ys) = no (λ ())
(x ∷ xs) ≟s [] = no (λ ())
(x ∷ xs) ≟s (y ∷ ys) = ∷-dec (x ≟ y) (xs ≟s ys)
where
∷-dec : {x y : A} {xs ys} Dec (x ≡ y) Dec (xs ≡ ys) Dec (x ∷ xs ≡ y ∷ ys)
∷-dec x≟y xs≟ys = map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment