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.Ex
import public Data.List.Map
import public Data.List.Set
import public Data.SortedMap
import public Decidable.Equality
import public Deriving.DepTyCheck.Gen.ForOneType.Interface
import public Deriving.DepTyCheck.Util.Specialisation

Definitions

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