Idris2Doc : Language.Reflection.TT

Language.Reflection.TT(source)

Reexports
import public Data.List
import public Data.String
Definitions
data Namespace : Type
  namespace, stored in reverse order

  Totality: total
  Visibility: public export
  Constructor: 
MkNS : List String -> Namespace

  Hints:
  
Biinjective NS
  
DecEq Namespace
  
Eq Namespace
  
Injective MkNS
  
Ord Namespace
  
Show Namespace
isParentOf : Namespace -> Namespace -> Bool
  Totality: total
  Visibility: export
data ModuleIdent : Type
  module identifier, stored in reverse order

  Totality: total
  Visibility: public export
  Constructor: 
MkMI : List String -> ModuleIdent
showSep : String -> List String -> String
  Totality: total
  Visibility: export
FilePos : Type
  'FilePos' represents the position of
  the source information in the file (or REPL).
  in the form of '(line-no, column-no)'.

  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
record WithFC : Type -> Type
  A wrapper for a value with a file context.

  Totality: total
  Visibility: public export
  Constructor: 
MkFCVal : FC -> ty -> WithFC ty

  Projections:
  
.fc : WithFC ty -> FC
  
.value : WithFC ty -> ty

  Hints:
  
Eq a => Eq (WithFC a)
  
Foldable WithFC
  
Functor WithFC
  
Ord a => Ord (WithFC a)
  
Traversable WithFC
.fc : WithFC ty -> FC
  Totality: total
  Visibility: public export
fc : WithFC ty -> FC
  Totality: total
  Visibility: public export
.value : WithFC ty -> ty
  Totality: total
  Visibility: public export
value : WithFC ty -> ty
  Totality: total
  Visibility: public export
NoFC : a -> WithFC a
  Smart constructor for WithFC that uses EmptyFC as location

  Totality: total
  Visibility: 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
  Any name that a user can assign to

  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
  A name in a Idris program

  Totality: total
  Visibility: public export
  Constructors:
  
NS : Namespace -> Name -> Name
  A qualified name
  
UN : UserName -> Name
  A user defined name
  
MN : String -> Int -> Name
  A machine generated name
  
DN : String -> Name -> Name
  A name with a display string
  
Nested : (Int, Int) -> Name -> Name
  Nested function name
  
CaseBlock : String -> Int -> Name
  Case block nested in (resolved) name
  
WithBlock : String -> Int -> Name
  With block nested in (resolved) name

  Hints:
  
Biinjective NS
  
Biinjective MN
  
Biinjective DN
  
Biinjective Nested
  
Biinjective CaseBlock
  
Biinjective WithBlock
  
DecEq Name
  
Eq Name
  
Injective UN
  
Ord Name
  
Show Name
fromName : Name -> Name
  Totality: total
  Visibility: public export
dropNS : Name -> Name
  Totality: total
  Visibility: export
getNS : Name -> Namespace
  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
  A multiplicity

  Totality: total
  Visibility: public export
  Constructors:
  
M0 : Count
  0 (erased)
  
M1 : Count
  1 (linear)
  
MW : Count
  ω (unrestricted)

  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

  Hints:
  
Eq a => Eq (PiInfo a)
  
Functor PiInfo
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