Idris2Doc : Language.Reflection.TT

Language.Reflection.TT

Reexports

importpublic Data.List
importpublic Data.String

Definitions

dataNamespace : Type
Totality: total
Visibility: public export
Constructor: 
MkNS : ListString->Namespace

Hints:
BiinjectiveNS
DecEqNamespace
EqNamespace
InjectiveMkNS
OrdNamespace
ShowNamespace
dataModuleIdent : Type
Totality: total
Visibility: public export
Constructor: 
MkMI : ListString->ModuleIdent
showSep : String->ListString->String
Totality: total
Visibility: export
FilePos : Type
Totality: total
Visibility: public export
dataVirtualIdent : Type
Totality: total
Visibility: public export
Constructor: 
Interactive : VirtualIdent
dataOriginDesc : Type
Totality: total
Visibility: public export
Constructors:
PhysicalIdrSrc : ModuleIdent->OriginDesc
  Anything that originates in physical Idris source files is assigned a
`PhysicalIdrSrc modIdent`,
where `modIdent` is the top-level module identifier of that file.
PhysicalPkgSrc : String->OriginDesc
  Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
where `fname` is path to the package file.
Virtual : VirtualIdent->OriginDesc
dataFC : Type
  A file context is a filename together with starting and ending positions.
It's often carried by AST nodes that might have been created from a source
file or by the compiler. That makes it useful to have the notion of
`EmptyFC` as part of the type.

Totality: total
Visibility: public export
Constructors:
MkFC : OriginDesc->FilePos->FilePos->FC
MkVirtualFC : OriginDesc->FilePos->FilePos->FC
  Virtual FCs are FC attached to desugared/generated code. They can help with marking
errors, but we shouldn't attach semantic highlighting metadata to them.
EmptyFC : FC
emptyFC : FC
Totality: total
Visibility: public export
dataNameType : Type
Totality: total
Visibility: public export
Constructors:
Bound : NameType
Func : NameType
DataCon : Int->Nat->NameType
TyCon : Int->Nat->NameType
dataPrimType : Type
Totality: total
Visibility: public export
Constructors:
IntType : PrimType
IntegerType : PrimType
Int8Type : PrimType
Int16Type : PrimType
Int32Type : PrimType
Int64Type : PrimType
Bits8Type : PrimType
Bits16Type : PrimType
Bits32Type : PrimType
Bits64Type : PrimType
StringType : PrimType
CharType : PrimType
DoubleType : PrimType
WorldType : PrimType

Hints:
EqPrimType
ShowPrimType
dataConstant : Type
Totality: total
Visibility: public export
Constructors:
I : Int->Constant
BI : Integer->Constant
I8 : Int8->Constant
I16 : Int16->Constant
I32 : Int32->Constant
I64 : Int64->Constant
B8 : Bits8->Constant
B16 : Bits16->Constant
B32 : Bits32->Constant
B64 : Bits64->Constant
Str : String->Constant
Ch : Char->Constant
Db : Double->Constant
PrT : PrimType->Constant
WorldVal : Constant

Hints:
EqConstant
ShowConstant
dataUserName : Type
Totality: total
Visibility: public export
Constructors:
Basic : String->UserName
Field : String->UserName
Underscore : UserName

Hints:
DecEqUserName
EqUserName
InjectiveBasic
InjectiveField
InjectiveUN
OrdUserName
ShowUserName
dataName : Type
Totality: total
Visibility: public export
Constructors:
NS : Namespace->Name->Name
UN : UserName->Name
MN : String->Int->Name
DN : String->Name->Name
Nested : (Int, Int) ->Name->Name
CaseBlock : String->Int->Name
WithBlock : String->Int->Name

Hints:
BiinjectiveNS
BiinjectiveMN
BiinjectiveDN
BiinjectiveNested
BiinjectiveCaseBlock
BiinjectiveWithBlock
DecEqName
EqName
InjectiveUN
OrdName
ShowName
dropNS : Name->Name
Totality: total
Visibility: export
isOp : Name->Bool
Totality: total
Visibility: export
showPrefix : Bool->Name->String
Totality: total
Visibility: export
recordNameInfo : Type
Totality: total
Visibility: public export
Constructor: 
MkNameInfo : NameType->NameInfo

Projection: 
.nametype : NameInfo->NameType
.nametype : NameInfo->NameType
Totality: total
Visibility: public export
nametype : NameInfo->NameType
Totality: total
Visibility: public export
dataCount : Type
Totality: total
Visibility: public export
Constructors:
M0 : Count
M1 : Count
MW : Count

Hints:
EqCount
OrdCount
enunciate : Count->String
Totality: total
Visibility: export
showCount : Count->String->String
Totality: total
Visibility: export
dataPiInfo : Type->Type
Totality: total
Visibility: public export
Constructors:
ImplicitArg : PiInfot
ExplicitArg : PiInfot
AutoImplicit : PiInfot
DefImplicit : t->PiInfot

Hint: 
Eqa=>Eq (PiInfoa)
showPiInfo : Showa=> {defaultTrue_ : Bool} ->PiInfoa->String->String
Totality: total
Visibility: export
dataIsVar : Name->Nat->ListName->Type
Totality: total
Visibility: public export
Constructors:
First : IsVarn0 (n::ns)
Later : IsVarnins->IsVarn (Si) (m::ns)
dataLazyReason : Type
Totality: total
Visibility: public export
Constructors:
LInf : LazyReason
LLazy : LazyReason
LUnknown : LazyReason

Hints:
EqLazyReason
ShowLazyReason
dataTotalReq : Type
Totality: total
Visibility: public export
Constructors:
Total : TotalReq
CoveringOnly : TotalReq
PartialOK : TotalReq

Hints:
EqTotalReq
ShowTotalReq
showTotalReq : MaybeTotalReq->String->String
Totality: total
Visibility: export
dataVisibility : Type
Totality: total
Visibility: public export
Constructors:
Private : Visibility
Export : Visibility
Public : Visibility

Hints:
EqVisibility
ShowVisibility
dataBuiltinType : Type
Totality: total
Visibility: public export
Constructors:
BuiltinNatural : BuiltinType
NaturalToInteger : BuiltinType
IntegerToNatural : BuiltinType

Hints:
EqBuiltinType
ShowBuiltinType