Language.Reflection.Compat.TypeInfo

Reexports

Definitions

.decl : TypeInfo -> Decl

  Generate a declaration from TypeInfo

Totality: total
Visibility: export

allInvolvedTypes : Elaboration m => Count -> TypeInfo -> m (List TypeInfo)

Totality: total
Visibility: export

ensureTyArgsNamed : Elaboration m => (ty : TypeInfo) -> m (AllTyArgsNamed ty)

Totality: total
Visibility: export

.argNames : (ti : TypeInfo) -> {auto 0 _ : AllTyArgsNamed ti} -> List Name

Totality: total
Visibility: export

record NamesInfoInTypes : Type

Totality: total
Visibility: export
Constructor: 

Names : ListMap Name TypeInfo -> ListMap Name (TypeInfo, Con) -> ListMap TypeInfo (SortedSet Name) -> NamesInfoInTypes

Projections:

.cons : NamesInfoInTypes -> ListMap Name (TypeInfo, Con)

.namesInTypes : NamesInfoInTypes -> ListMap TypeInfo (SortedSet Name)

.types : NamesInfoInTypes -> ListMap Name TypeInfo

Hints:

Monoid NamesInfoInTypes

Semigroup NamesInfoInTypes

lookupType : NamesInfoInTypes => Name -> Maybe TypeInfo

Totality: total
Visibility: export

lookupCon : NamesInfoInTypes => Name -> Maybe Con

Totality: total
Visibility: export

knownTypes : NamesInfoInTypes => ListMap Name TypeInfo

Totality: total
Visibility: export

resolveNamesUniquely : NamesInfoInTypes => SortedSet Name -> TTImp -> Either (Name, SortedSet Name) TTImp

  Returns either resolved expression, or a non-unique name and the set of alternatives.

Totality: total
Visibility: export

hasNameInsideDeep : NamesInfoInTypes => Name -> TTImp -> Bool

Totality: total
Visibility: export

isRecursive : NamesInfoInTypes => Con -> {default Nothing _ : Maybe TypeInfo} -> Bool

Totality: total
Visibility: export

isRecursiveConstructor : NamesInfoInTypes => Name -> Maybe Bool

Totality: total
Visibility: export

enrichNamesInfoInTypes : Elaboration m => List TypeInfo -> NamesInfoInTypes -> m NamesInfoInTypes

Totality: total
Visibility: export

getNamesInfoInTypes : Elaboration m => TypeInfo -> m NamesInfoInTypes

Totality: total
Visibility: export

getNamesInfoInTypes' : Elaboration m => TTImp -> m NamesInfoInTypes

Totality: total
Visibility: export