Idris2Doc : Language.Reflection.TT

Language.Reflection.TT

dataBuiltinType : Type
Totality: total
Constructors:
BuiltinNatural : BuiltinType
NaturalToInteger : BuiltinType
IntegerToNatural : BuiltinType
dataConstant : Type
Totality: total
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
WorldVal : Constant
IntType : Constant
IntegerType : Constant
Int8Type : Constant
Int16Type : Constant
Int32Type : Constant
Int64Type : Constant
Bits8Type : Constant
Bits16Type : Constant
Bits32Type : Constant
Bits64Type : Constant
StringType : Constant
CharType : Constant
DoubleType : Constant
WorldType : Constant
dataCount : Type
Totality: total
Constructors:
M0 : Count
M1 : Count
MW : Count
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
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
FilePos : Type
Totality: total
dataIsVar : Name -> Nat -> ListName -> Type
Totality: total
Constructors:
First : IsVarn0 (n::ns)
Later : IsVarnins -> IsVarn (Si) (m::ns)
dataLazyReason : Type
Totality: total
Constructors:
LInf : LazyReason
LLazy : LazyReason
LUnknown : LazyReason
dataModuleIdent : Type
Totality: total
Constructor: 
MkMI : ListString -> ModuleIdent
dataName : Type
Totality: total
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
dataNameType : Type
Totality: total
Constructors:
Bound : NameType
Func : NameType
DataCon : Int -> Nat -> NameType
TyCon : Int -> Nat -> NameType
dataNamespace : Type
Totality: total
Constructor: 
MkNS : ListString -> Namespace
dataOriginDesc : Type
Totality: total
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
dataPiInfo : Type -> Type
Totality: total
Constructors:
ImplicitArg : PiInfot
ExplicitArg : PiInfot
AutoImplicit : PiInfot
DefImplicit : t -> PiInfot
dataTT : Type
Totality: total
dataTotalReq : Type
Totality: total
Constructors:
Total : TotalReq
CoveringOnly : TotalReq
PartialOK : TotalReq
dataUserName : Type
Totality: total
Constructors:
Basic : String -> UserName
Field : String -> UserName
Underscore : UserName
dataVirtualIdent : Type
Totality: total
Constructor: 
Interactive : VirtualIdent
dataVisibility : Type
Totality: total
Constructors:
Private : Visibility
Export : Visibility
Public : Visibility
emptyFC : FC
Totality: total
showSep : String -> ListString -> String
Totality: total