Language.Reflection.TT

Reexports

Definitions

data Namespace : Type

Totality: total
Visibility: public export
Constructor: 

MkNS : List String -> Namespace

Hints:

Biinjective NS

DecEq Namespace

Eq Namespace

Injective MkNS

Ord Namespace

Show Namespace

data ModuleIdent : Type

Totality: total
Visibility: public export
Constructor: 

MkMI : List String -> ModuleIdent

showSep : String -> List String -> String

Totality: total
Visibility: export

FilePos : Type

Totality: total
Visibility: public export

data VirtualIdent : Type

Totality: total
Visibility: public export
Constructor: 

Interactive : VirtualIdent

data OriginDesc : 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

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
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

data NameType : Type

Totality: total
Visibility: public export
Constructors:

Bound : NameType

Func : NameType

DataCon : Int -> Nat -> NameType

TyCon : Int -> Nat -> NameType

data PrimType : 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:

Eq PrimType

Show PrimType

data Constant : 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:

Eq Constant

Show Constant

data UserName : Type

Totality: total
Visibility: public export
Constructors:

Basic : String -> UserName

Field : String -> UserName

Underscore : UserName

Hints:

DecEq UserName

Eq UserName

Injective Basic

Injective Field

Injective UN

Ord UserName

Show UserName

data Name : 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:

Biinjective NS

Biinjective MN

Biinjective DN

Biinjective Nested

Biinjective CaseBlock

Biinjective WithBlock

DecEq Name

Eq Name

Injective UN

Ord Name

Show Name

dropNS : Name -> Name

Totality: total
Visibility: export

isOp : Name -> Bool

Totality: total
Visibility: export

showPrefix : Bool -> Name -> String

Totality: total
Visibility: export

record NameInfo : 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

data Count : Type

Totality: total
Visibility: public export
Constructors:

M0 : Count

M1 : Count

MW : Count

Hints:

Eq Count

Ord Count

enunciate : Count -> String

Totality: total
Visibility: export

showCount : Count -> String -> String

Totality: total
Visibility: export

data PiInfo : Type -> Type

Totality: total
Visibility: public export
Constructors:

ImplicitArg : PiInfo t

ExplicitArg : PiInfo t

AutoImplicit : PiInfo t

DefImplicit : t -> PiInfo t

Hint: 

Eq a => Eq (PiInfo a)

showPiInfo : Show a => {default True _ : Bool} -> PiInfo a -> String -> String

Totality: total
Visibility: export

data IsVar : Name -> Nat -> List Name -> Type

Totality: total
Visibility: public export
Constructors:

First : IsVar n 0 (n :: ns)

Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

data LazyReason : Type

Totality: total
Visibility: public export
Constructors:

LInf : LazyReason

LLazy : LazyReason

LUnknown : LazyReason

Hints:

Eq LazyReason

Show LazyReason

data TotalReq : Type

Totality: total
Visibility: public export
Constructors:

Total : TotalReq

CoveringOnly : TotalReq

PartialOK : TotalReq

Hints:

Eq TotalReq

Show TotalReq

showTotalReq : Maybe TotalReq -> String -> String

Totality: total
Visibility: export

data Visibility : Type

Totality: total
Visibility: public export
Constructors:

Private : Visibility

Export : Visibility

Public : Visibility

Hints:

Eq Visibility

Show Visibility

data BuiltinType : Type

Totality: total
Visibility: public export
Constructors:

BuiltinNatural : BuiltinType

NaturalToInteger : BuiltinType

IntegerToNatural : BuiltinType

Hints:

Eq BuiltinType

Show BuiltinType