Idris2Doc : Search.HDecidable

Search.HDecidable

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
(&&) : (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
interfaceAnHDec : (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
recordHDec : Type -> Type
  Half a decider: when the search succeeds we bother building the proof

Totality: total
Constructor: 
MkHDec : (isTrue : Bool) -> (SoisTrue -> a) -> HDeca

Projections:
.evidence : (rec : HDeca) -> So (isTruerec) -> a
.isTrue : HDeca -> Bool
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