Idris2Doc : Deriving.DepTyCheck.Gen.ConsRecs

Deriving.DepTyCheck.Gen.ConsRecs

(source)
Reexports
import public Data.Alternative
import public Data.Fuel
import public Data.List.Ex
import public Data.List.Map
import public Data.Nat1
import public Data.SortedMap
import public Data.SortedMap.Extra
import public Data.SortedSet
import public Data.SortedSet.Extra
import public Deriving.DepTyCheck.Gen.Signature
import public Deriving.DepTyCheck.Gen.Tuning
import public Language.Reflection.Compat.TypeInfo
import public Language.Reflection.Logging
import public Syntax.IHateParens.Function
Definitions
data RecWeightInfo : Type
  Weight info of recursive constructors

  Totality: total
  Visibility: public export
  Constructors:
  
SpendingFuel : (Name -> TTImp) -> RecWeightInfo
  
StructurallyDecreasing : TypeInfo -> TTImp -> RecWeightInfo
record ConWeightInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkConWeightInfo : Either Nat1 RecWeightInfo -> ConWeightInfo

  Projection: 
.weight : ConWeightInfo -> Either Nat1 RecWeightInfo
  Either a constant (for non-recursive) or a function returning weight info (for recursive)
.weight : ConWeightInfo -> Either Nat1 RecWeightInfo
  Either a constant (for non-recursive) or a function returning weight info (for recursive)

  Totality: total
  Visibility: public export
weight : ConWeightInfo -> Either Nat1 RecWeightInfo
  Either a constant (for non-recursive) or a function returning weight info (for recursive)

  Totality: total
  Visibility: public export
reflectNat1 : Nat1 -> TTImp
  Totality: total
  Visibility: export
isWeight1 : TTImp -> Bool
  Totality: total
  Visibility: export
weightExpr : ConWeightInfo -> Either TTImp (Name -> TTImp)
  Totality: total
  Visibility: public export
usedWeightFun : ConWeightInfo -> Maybe TypeInfo
  Totality: total
  Visibility: export
record ConsRecs : Type
  Totality: total
  Visibility: export
  Constructor: 
MkConsRecs : SortedMap Name TyConsRec -> ConsRecs

  Projection: 
.consRecs : ConsRecs -> SortedMap Name TyConsRec

  Hint: 
Semigroup ConsRecs
interimNamesWrapper : Name -> Name
  Totality: total
  Visibility: export
leftDepth : Fuel -> Nat1
  Totality: total
  Visibility: public export
getConsRecs : NamesInfoInTypes => Elaboration m => m ConsRecs
  Totality: total
  Visibility: export
lookupConsWithWeight : ConsRecs => NamesInfoInTypes => GenSignature -> Maybe (List (Con, ConWeightInfo))
  Totality: total
  Visibility: export
deriveWeightingFun : ConsRecs => TypeInfo -> Maybe (Decl, Decl)
  Totality: total
  Visibility: export
isTypeKnown : ConsRecs => TypeInfo -> Bool
  Totality: total
  Visibility: export
updateNamesAndConsRecs : NamesInfoInTypes => ConsRecs => Elaboration m => List TypeInfo -> m (NamesInfoInTypes, ConsRecs)
  Totality: total
  Visibility: export