Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/DecEq.agda Secret

Created September 1, 2017 14:31
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/a40dbb19e05fc2fe368f8ee6dbcd4f9f to your computer and use it in GitHub Desktop.
Save mietek/a40dbb19e05fc2fe368f8ee6dbcd4f9f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
DecEq.agda
infixr 7 _⇒_
data Ty : Set where
o : Ty
_⇒_ : Ty → Ty → Ty
⇒-inj₁ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
⇒-inj₁ refl = refl
⇒-inj₂ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
⇒-inj₂ refl = refl
_≟_ : (A A′ : Ty) → Dec (A ≡ A′)
o ≟ o = yes refl
o ≟ (A′ ⇒ B′) = no λ ()
(A ⇒ B) ≟ o = no λ ()
(A ⇒ B) ≟ (A′ ⇒ B′) with A ≟ A′ | B ≟ B′
... | yes refl | yes refl = yes refl
... | no A≢A′ | _ = no (A≢A′ ∘ ⇒-inj₁)
... | _ | no B≢B′ = no (B≢B′ ∘ ⇒-inj₂)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment