everything.ced

module everything.

-- utilies
import utils.

-- recursive types
import cast.
import mono.
import recType.

-- functors
import functor.
import functorThms.

-- recursion schemes
import data-char as Char .

-- derivation of Scott-encoded naturals
import scott/concrete/nat as SN .

-- generic derivation of Scott-encoded data
import scott as S.

-- derivation of Parigot-encoded naturals
import parigot/concrete/nat as NP.

-- generic derivation of Parigot-encoded data
import parigot as P.

-- examples of generic Parigot encodings

import parigot/examples/list-data as LP .
import parigot/examples/list as LP .
import parigot/examples/rosetree-data as RTP .

-- Lepigre-Raffalli naturals
import lepigre-raffalli/concrete/nat1 as LRN1 .
import lepigre-raffalli/concrete/nat2 as LRN2 .

-- generic Lepigre-Raffalli encoding
import lepigre-raffalli as LR.

-- monotone type schemes strictly contain functorial type schemes
import signatures/itree .