module Data.Dec.Base where
Decidable typesπ
The type Dec
, of
decisions for a type A
, is a renaming of
the coproduct A + Β¬ A
. A value of Dec A
witnesses not that A
is decidable, but that it has been
decided; A witness of decidability, then, is a proof assigning
decisions to values of a certain type.
data Dec {β} (A : Type β) : Type β where yes : (a : A) β Dec A no : (Β¬a : Β¬ A) β Dec A Dec-elim : β {β β'} {A : Type β} (P : Dec A β Type β') β (β y β P (yes y)) β (β y β P (no y)) β β x β P x Dec-elim P f g (yes x) = f x Dec-elim P f g (no x) = g x
recover : β {β} {A : Type β} β Dec A β .A β A recover (yes x) _ = x recover {A = A} (no Β¬x) x = go (Β¬x x) where go : .β₯ β A go ()
A type is discrete if it has decidable equality.
Discrete : β {β} β Type β β Type β Discrete A = (x y : A) β Dec (x β‘ y)