Idris2Doc : Deriving.DepTyCheck.Util.Specialisation

Deriving.DepTyCheck.Util.Specialisation

(source)
Reexports
import public Control.Monad.Either
import public Data.DPair
import public Data.List.Ex
import public Data.List.Map
import public Data.SortedMap
import public Data.SortedMap.Extra
import public Data.SortedSet
import public Deriving.DepTyCheck.Gen.ForOneType.Interface
import public Deriving.SpecialiseData
import public Deriving.SpecialiseData.TaskFormation
import public Language.Reflection.Unify
import public Data.Hashable
import public Data.Hashable.Base
Definitions
formGivenVals : (s : SortedSet {_:8478}) -> List TTImp -> Vect (s .size) TTImp
  Given a set of given argument indices, convert a list of their values into a vector that can be fed to `callGen`
  
  The values should be listed for indices in ascending order
  (i.e. how these indices would be sorted if we called `toList` on the set)

  Totality: total
  Visibility: export
specialiseIfNeeded : Elaboration m => NamesInfoInTypes => ConsRecs => DerivationClosure m => (sig : GenSignature) -> TTImp -> Vect ((sig .givenParams) .size) TTImp -> m (Maybe TTImp)
  Totality: total
  Visibility: export