Data.Container.Base.Concrete.Definition

Definitions

interface FromConcrete : Cont -> Type

  Many Idris' datatypes are already concrete, inductive
  representations of particular containers
  It is useful to be easily able to convert between them

Parameters: cont
Constructor: 

MkConcrete

Methods:

concreteType : Type -> Type

concreteFunctor : Functor concreteType

fromConcreteTy : concreteType a -> Ext cont a

toConcreteTy : Ext cont a -> concreteType a

Implementations:

FromConcrete Scalar

FromConcrete Maybe

FromConcrete List

FromConcrete (Vect n)

FromConcrete BinTree

FromConcrete BinTreeNode

FromConcrete BinTreeLeaf

concreteType : FromConcrete cont => Type -> Type

Visibility: public export

concreteFunctor : {auto __con : FromConcrete cont} -> Functor concreteType

Visibility: public export

fromConcreteTy : {auto __con : FromConcrete cont} -> concreteType a -> Ext cont a

Visibility: public export

toConcreteTy : {auto __con : FromConcrete cont} -> Ext cont a -> concreteType a

Visibility: public export

data AllConcrete : List Cont -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllConcrete []

Cons : FromConcrete c => AllConcrete cs => AllConcrete (c :: cs)