Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface

Reexports

Definitions

interface DerivationClosure : (Type -> Type) -> Type

Parameters: m
Constraints: Monad m
Methods:

callGen : NamesInfoInTypes => ConsRecs => (sig : GenSignature) -> TTImp -> Vect ((sig .givenParams) .size) TTImp -> m (TTImp, Maybe (gend : Nat ** Vect gend (Fin gend)))

Implementations:

DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignature (ExternalGenSignature, Name) => DerivationClosure m

DerivationClosure m => MonadTrans t => Monad (t m) => DerivationClosure (t m)

callGen : DerivationClosure m => NamesInfoInTypes => ConsRecs => (sig : GenSignature) -> TTImp -> Vect ((sig .givenParams) .size) TTImp -> m (TTImp, Maybe (gend : Nat ** Vect gend (Fin gend)))

Totality: total
Visibility: public export

outmostFuelArg : Name

Totality: total
Visibility: export