Idris2Doc : Language.Reflection.TT

Language.Reflection.TT

data BuiltinType : Type
  Totality: total
  Constructors:
  
BuiltinNatural : BuiltinType
  
NaturalToInteger : BuiltinType
  
IntegerToNatural : BuiltinType
data Constant : 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
data Count : Type
  Totality: total
  Constructors:
  
M0 : Count
  
M1 : Count
  
MW : Count
data FC : 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
data IsVar : Name -> Nat -> List Name -> Type
  Totality: total
  Constructors:
  
First : IsVar n 0 (n :: ns)
  
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
data LazyReason : Type
  Totality: total
  Constructors:
  
LInf : LazyReason
  
LLazy : LazyReason
  
LUnknown : LazyReason
data ModuleIdent : Type
  Totality: total
  Constructor: 
MkMI : List String -> ModuleIdent
data Name : 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
data NameType : Type
  Totality: total
  Constructors:
  
Bound : NameType
  
Func : NameType
  
DataCon : Int -> Nat -> NameType
  
TyCon : Int -> Nat -> NameType
data Namespace : Type
  Totality: total
  Constructor: 
MkNS : List String -> Namespace
data OriginDesc : 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
data PiInfo : Type -> Type
  Totality: total
  Constructors:
  
ImplicitArg : PiInfo t
  
ExplicitArg : PiInfo t
  
AutoImplicit : PiInfo t
  
DefImplicit : t -> PiInfo t
data TT : Type
  Totality: total
data TotalReq : Type
  Totality: total
  Constructors:
  
Total : TotalReq
  
CoveringOnly : TotalReq
  
PartialOK : TotalReq
data UserName : Type
  Totality: total
  Constructors:
  
Basic : String -> UserName
  
Field : String -> UserName
  
Underscore : UserName
data VirtualIdent : Type
  Totality: total
  Constructor: 
Interactive : VirtualIdent
data Visibility : Type
  Totality: total
  Constructors:
  
Private : Visibility
  
Export : Visibility
  
Public : Visibility
emptyFC : FC
  Totality: total
showSep : String -> List String -> String
  Totality: total