Skip to content

Instantly share code, notes, and snippets.

@MarcelineVQ
Created January 2, 2020 10:10
Show Gist options
  • Select an option

  • Save MarcelineVQ/e7d6d4bcc8873343936e6e62d5121022 to your computer and use it in GitHub Desktop.

Select an option

Save MarcelineVQ/e7d6d4bcc8873343936e6e62d5121022 to your computer and use it in GitHub Desktop.
data ExactlyOne {A : Set} : (xs : List A) → Set where
TheOne : ∀ {x} → ExactlyOne (x ∷ [])
exactlyOne : ∀ {a} → (xs : List a) → Dec (ExactlyOne xs)
exactlyOne [] = no (λ ())
exactlyOne (x ∷ []) = yes TheOne
exactlyOne (x ∷ y ∷ xs) = no λ ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment