- (&&) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (a, b)
Half deciders are closed under product
Totality: total
Fixity Declaration: infixr operator, level 5- (==>) : (AnHDec l, (AnHDec r, Negates na a)) => l na -> r b -> HDec (a -> b)
Half deciders are closed under implication
Totality: total
Fixity Declaration: infixr operator, level 3- interface AnHDec : (Type -> Type) -> Type
A type constructor satisfying AnHdec is morally an HDec i.e. we can
turn values of this type constructor into half deciders
It may be more powerful (like Dec) or more basic (like Maybe).
Parameters: t
Methods:
- toHDec : t a -> HDec a
Implementations:
- AnHDec Dec
- AnHDec HDec
- AnHDec Maybe
- record HDec : Type -> Type
Half a decider: when the search succeeds we bother building the proof
Totality: total
Constructor: - MkHDec : (isTrue : Bool) -> (So isTrue -> a) -> HDec a
Projections:
- .evidence : (rec : HDec a) -> So (isTrue rec) -> a
- .isTrue : HDec a -> Bool
- fromDec : Dec a -> HDec a
- Totality: total
- fromMaybe : Maybe a -> HDec a
- Totality: total
- no : HDec a
Giving up
Totality: total- not : (AnHDec l, Negates na a) => l na -> HDec (Not a)
Half deciders are closed negation. Here we use the `Negates` interface
so that we end up looking for *positive* evidence of something which is
much easier to find than negative one.
Totality: total- toHDec : AnHDec t => t a -> HDec a
- Totality: total
- toMaybe : HDec a -> Maybe a
- Totality: total
- yes : a -> HDec a
Happy path: we have found a proof!
Totality: total- (||) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (Either a b)
Half deciders are closed under sum
Totality: total
Fixity Declaration: infixr operator, level 4