Idris2Doc : Language.Reflection.TTImp

Language.Reflection.TTImp

AltType : Type
Totality: total
Constructors:
FirstSuccess : AltType
Unique : AltType
UniqueDefault : TTImp -> AltType
BindMode : Type
Totality: total
Constructors:
PI : Count -> BindMode
PATTERN : BindMode
NONE : BindMode
Clause : Type
Totality: total
Constructors:
PatClause : FC -> TTImp -> TTImp -> Clause
WithClause : FC -> TTImp -> TTImp -> ListClause -> Clause
ImpossibleClause : FC -> TTImp -> Clause
Data : Type
Totality: total
Constructors:
MkData : FC -> Name -> TTImp -> ListDataOpt -> ListITy -> Data
MkLater : FC -> Name -> TTImp -> Data
DataOpt : Type
Totality: total
Constructors:
SearchBy : ListName -> DataOpt
NoHints : DataOpt
UniqueSearch : DataOpt
External : DataOpt
NoNewtype : DataOpt
Decl : Type
Totality: total
Constructors:
IClaim : FC -> Count -> Visibility -> ListFnOpt -> ITy -> Decl
IData : FC -> Visibility -> Data -> Decl
IDef : FC -> Name -> ListClause -> Decl
IParameters : FC -> List (Name, TTImp) -> ListDecl -> Decl
IRecord : FC -> Visibility -> Record -> Decl
INamespace : FC -> Namespace -> ListDecl -> Decl
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
ILog : Nat -> Decl
DotReason : Type
Totality: total
Constructors:
NonLinearVar : DotReason
VarApplied : DotReason
NotConstructor : DotReason
ErasedArg : DotReason
UserDotted : DotReason
UnknownDot : DotReason
UnderAppliedCon : DotReason
FnOpt : Type
Totality: total
Constructors:
Inline : FnOpt
TCInline : FnOpt
Hint : Bool -> FnOpt
GlobalHint : Bool -> FnOpt
ExternFn : FnOpt
ForeignFn : ListTTImp -> FnOpt
Invertible : FnOpt
Totality : TotalReq -> FnOpt
Macro : FnOpt
SpecArgs : ListName -> FnOpt
IField : Type
Totality: total
Constructor: 
MkIField : FC -> Count -> PiInfoTTImp -> Name -> TTImp -> IField
IFieldUpdate : Type
Totality: total
Constructors:
ISetField : List String -> TTImp -> IFieldUpdate
ISetFieldApp : List String -> TTImp -> IFieldUpdate
ITy : Type
Totality: total
Constructor: 
MkTy : FC -> FC -> Name -> TTImp -> ITy
Record : Type
Totality: total
Constructor: 
MkRecord : FC -> Name -> List (Name, TTImp) -> Name -> ListIField -> Record
TTImp : Type
Totality: total
Constructors:
IVar : FC -> Name -> TTImp
IPi : FC -> Count -> PiInfoTTImp -> MaybeName -> TTImp -> TTImp -> TTImp
ILam : FC -> Count -> PiInfoTTImp -> MaybeName -> TTImp -> TTImp -> TTImp
ILet : FC -> FC -> Count -> Name -> TTImp -> TTImp -> TTImp -> TTImp
ICase : FC -> TTImp -> TTImp -> ListClause -> TTImp
ILocal : FC -> ListDecl -> TTImp -> TTImp
IUpdate : FC -> ListIFieldUpdate -> TTImp -> TTImp
IApp : FC -> TTImp -> TTImp -> TTImp
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
IAutoApp : FC -> TTImp -> TTImp -> TTImp
IWithApp : FC -> TTImp -> TTImp -> TTImp
ISearch : FC -> Nat -> TTImp
IAlternative : FC -> AltType -> ListTTImp -> TTImp
IRewrite : FC -> TTImp -> TTImp -> TTImp
IBindHere : FC -> BindMode -> TTImp -> TTImp
IBindVar : FC -> String -> TTImp
IAs : FC -> FC -> UseSide -> Name -> TTImp -> TTImp
IMustUnify : FC -> DotReason -> TTImp -> TTImp
IDelayed : FC -> LazyReason -> TTImp -> TTImp
IDelay : FC -> TTImp -> TTImp
IForce : FC -> TTImp -> TTImp
IQuote : FC -> TTImp -> TTImp
IQuoteName : FC -> Name -> TTImp
IQuoteDecl : FC -> TTImp -> TTImp
IUnquote : FC -> TTImp -> TTImp
IPrimVal : FC -> Constant -> TTImp
IType : FC -> TTImp
IHole : FC -> String -> TTImp
Implicit : FC -> Bool -> TTImp
IWithUnambigNames : FC -> ListName -> TTImp -> TTImp
UseSide : Type
Totality: total
Constructors:
UseLeft : UseSide
UseRight : UseSide