Deriving.SpecialiseData.TaskFormation

Reexports

Definitions

record GenArg : Type

  Information about a generator's argument extracted from GenSignature

Totality: total
Visibility: public export
Constructor: 

MkGenArg : Arg -> Maybe TTImp -> GenArg

Projections:

.arg : GenArg -> Arg

  Formal argument beloging to a type constructor

.given : GenArg -> Maybe TTImp

  Value of the actual/given argument (if present)

Hint: 

LogPosition GenArg

.arg : GenArg -> Arg

  Formal argument beloging to a type constructor

Visibility: public export

arg : GenArg -> Arg

  Formal argument beloging to a type constructor

Visibility: public export

.given : GenArg -> Maybe TTImp

  Value of the actual/given argument (if present)

Visibility: public export

given : GenArg -> Maybe TTImp

  Value of the actual/given argument (if present)

Visibility: public export

data ArgDecision : Type

Totality: total
Visibility: public export
Constructors:

Passthrough : ArgDecision

SpecLit : TTImp -> ArgDecision

SpecRec : Name -> List GenArg -> ArgDecision

specDecideArg : NamesInfoInTypes => GenArg -> (ArgDecision, String)

Visibility: export

argsToSpecTask : MonadLog m => NamesInfoInTypes => (GenArg -> (ArgDecision, String)) -> Name -> List GenArg -> m (TTImp, (List Arg, List (Maybe TTImp)))

Visibility: export

exprToSpecTask : MonadLog m => NamesInfoInTypes => (GenArg -> (ArgDecision, String)) -> TTImp -> m (Maybe (TTImp, (List Arg, List (Maybe TTImp))))

Visibility: export