Idris2Doc : Deriving.DepTyCheck.Gen.ForAllNeededTypes.Impl

Deriving.DepTyCheck.Gen.ForAllNeededTypes.Impl

(source)
A bridge between a single act of derivation (for a single type) and a user derivation task

Reexports

import public Control.Monad.State
import public Data.DPair
import public Data.List.Set
import public Data.SortedMap
import public Decidable.Equality
import public Deriving.DepTyCheck.Gen.ForOneType.Interface

Definitions

runCanonic : DeriveBodyForType => NamesInfoInTypes => ConsRecs => SortedMap ExternalGenSignature Name -> (DerivationClosure m => m a) -> Elab (a, List Decl)
Totality: total
Visibility: export