Control.DivideAndConquer

(source)

The content of this module is based on the paper
A Type-Based Approach to Divide-And-Conquer Recursion in Coq
by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
J. Garret Morris, and Aaron Stump
https://doi.org/10.1145/3571196

The original paper relies on Coq's impredicative Set axiom,
something we don't have access to in Idris 2. We can however
reproduce the results by ignoring the type levels

Definitions

data ListF : Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : ListF a x
(::) : a -> x -> ListF a x

Hint:

Functor (ListF a)

data Mu : (Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor:

MkMu : (r -> Mu f) -> f r -> Mu f

inMu : f (Mu f) -> Mu f

Totality: total
Visibility: public export

outMu : Functor f => Mu f -> f (Mu f)

Totality: total
Visibility: public export

fold : Functor f => (f a -> a) -> Mu f -> a

Totality: total
Visibility: public export

KAlg : Type

Totality: total
Visibility: public export

0 Mono : (KAlg -> KAlg) -> Type

Totality: total
Visibility: public export

data Mu : (KAlg -> KAlg) -> KAlg

Totality: total
Visibility: public export
Constructor:

MkMu : (a x -> Mu f x) -> f a x -> Mu f x

inMu : f (Mu f) x -> Mu f x

Totality: total
Visibility: public export

outMu : Mono f -> Mu f x -> f (Mu f) x

Totality: total
Visibility: public export

0 FoldT : (0 _ : (Type -> Type)) -> KAlg -> Type -> Type

Totality: total
Visibility: public export

0 SAlgF : (0 _ : (Type -> Type)) -> KAlg -> (Type -> Type) -> Type

Totality: total
Visibility: public export

0 SAlg : (0 _ : (Type -> Type)) -> (Type -> Type) -> Type

Totality: total
Visibility: public export

0 AlgF : (0 _ : (Type -> Type)) -> KAlg -> (Type -> Type) -> Type

Totality: total
Visibility: public export

0 Alg : (0 _ : (Type -> Type)) -> (Type -> Type) -> Type

Totality: total
Visibility: public export

inSAlg : (0 f : (Type -> Type)) -> SAlgF SAlg x -> SAlg x

Totality: total
Visibility: public export

monoSAlgF : (0 f : (Type -> Type)) -> Mono SAlgF

Totality: total
Visibility: public export

outSAlg : (0 f : (Type -> Type)) -> SAlg x -> SAlgF SAlg x

Totality: total
Visibility: public export

inAlg : (0 f : (Type -> Type)) -> AlgF Alg x -> Alg x

Totality: total
Visibility: public export

monoAlgF : (0 f : (Type -> Type)) -> Mono AlgF

Totality: total
Visibility: public export

outAlg : (0 f : (Type -> Type)) -> Alg x -> AlgF Alg x

Totality: total
Visibility: public export

0 DcF : (0 _ : (Type -> Type)) -> Type -> Type

Totality: total
Visibility: public export

functorDcF : (0 f : (Type -> Type)) -> Functor DcF

Totality: total
Visibility: public export

0 Dc : (0 _ : (Type -> Type)) -> Type

Totality: total
Visibility: public export

fold : (0 f : (Type -> Type)) -> FoldT Alg Dc

Totality: total
Visibility: public export

record RevealT : (0 _ : (Type -> Type)) -> (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructor:

MkRevealT : (0 f : (Type -> Type)) -> ((r -> Dc) -> x Dc) -> RevealT x r

Projection:

.runRevealT : (0 f : (Type -> Type)) -> RevealT x r -> (r -> Dc) -> x Dc

Hint:

(0 f : (Type -> Type)) -> Functor (RevealT x)

.runRevealT : (0 f : (Type -> Type)) -> RevealT x r -> (r -> Dc) -> x Dc

Totality: total
Visibility: public export

runRevealT : (0 f : (Type -> Type)) -> RevealT x r -> (r -> Dc) -> x Dc

Totality: total
Visibility: public export

functorRevealT : (0 f : (Type -> Type)) -> Functor (RevealT x)

Totality: total
Visibility: public export

promote : (0 f : (Type -> Type)) -> Functor x => SAlg x -> Alg (RevealT x)

Totality: total
Visibility: public export

sfold : (0 f : (Type -> Type)) -> FoldT SAlg Dc

Totality: total
Visibility: public export

inDc : (0 f : (Type -> Type)) -> f Dc -> Dc

Totality: total
Visibility: public export

0 list : Type -> Type

Totality: total
Visibility: public export

Nil : list a

Totality: total
Visibility: public export

(::) : a -> list a -> list a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

fromList : List a -> list a

Totality: total
Visibility: public export

0 SpanF : Type -> Type -> Type

Totality: total
Visibility: public export

spanr : FoldT SAlg r -> (a -> Bool) -> r -> SpanF a r

Totality: total
Visibility: export

zero : Nat -> Nat

Totality: total
Visibility: export

matchExample : Bool

Totality: total
Visibility: export

sortExample : String -> String

Totality: total
Visibility: export