Idris2Doc : Search.HDecidable

Search.HDecidable

(&&) : (AnHDecl, AnHDecr) => la -> rb -> HDec (a, b)
Half deciders are closed under product
Totality: total
Fixity Declaration: infixr operator, level 5
(==>) : (AnHDecl, (AnHDecr, Negatesnaa)) => lna -> rb -> HDec (a -> b)
Half deciders are closed under implication
Totality: total
Fixity Declaration: infixr operator, level 3
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 : ta -> HDeca

Implementations:
AnHDecDec
AnHDecHDec
AnHDecMaybe
HDec : Type -> Type
Half a decider: when the search succeeds we bother building the proof
Totality: total
Constructor: 
fromDec : Deca -> HDeca
Totality: total
fromMaybe : Maybea -> HDeca
Totality: total
no : HDeca
Giving up
Totality: total
not : (AnHDecl, Negatesnaa) => lna -> HDec (Nota)
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 : AnHDect => ta -> HDeca
Totality: total
toMaybe : HDeca -> Maybea
Totality: total
yes : a -> HDeca
Happy path: we have found a proof!
Totality: total
(||) : (AnHDecl, AnHDecr) => la -> rb -> HDec (Eitherab)
Half deciders are closed under sum
Totality: total
Fixity Declaration: infixr operator, level 4