Idris2Doc : Language.Reflection.TTImp

Language.Reflection.TTImp

dataAltType : Type
Totality: total
Constructors:
FirstSuccess : AltType
Unique : AltType
UniqueDefault : TTImp -> AltType
dataBindMode : Type
Totality: total
Constructors:
PI : Count -> BindMode
PATTERN : BindMode
NONE : BindMode
dataClause : Type
Totality: total
Constructors:
PatClause : FC -> TTImp -> TTImp -> Clause
WithClause : FC -> TTImp -> TTImp -> MaybeName -> ListWithFlag -> ListClause -> Clause
ImpossibleClause : FC -> TTImp -> Clause
dataData : Type
Totality: total
Constructors:
MkData : FC -> Name -> TTImp -> ListDataOpt -> ListITy -> Data
MkLater : FC -> Name -> TTImp -> Data
dataDataOpt : Type
Totality: total
Constructors:
SearchBy : ListName -> DataOpt
NoHints : DataOpt
UniqueSearch : DataOpt
External : DataOpt
NoNewtype : DataOpt
dataDecl : 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, (Count, (PiInfoTTImp, TTImp))) -> ListDecl -> Decl
IRecord : FC -> MaybeString -> Visibility -> Record -> Decl
INamespace : FC -> Namespace -> ListDecl -> Decl
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
IRunElabDecl : FC -> TTImp -> Decl
ILog : Maybe (ListString, Nat) -> Decl
IBuiltin : FC -> BuiltinType -> Name -> Decl
dataDotReason : Type
Totality: total
Constructors:
NonLinearVar : DotReason
VarApplied : DotReason
NotConstructor : DotReason
ErasedArg : DotReason
UserDotted : DotReason
UnknownDot : DotReason
UnderAppliedCon : DotReason
dataFnOpt : 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
dataIField : Type
Totality: total
Constructor: 
MkIField : FC -> Count -> PiInfoTTImp -> Name -> TTImp -> IField
dataIFieldUpdate : Type
Totality: total
Constructors:
ISetField : ListString -> TTImp -> IFieldUpdate
ISetFieldApp : ListString -> TTImp -> IFieldUpdate
dataITy : Type
Totality: total
Constructor: 
MkTy : FC -> FC -> Name -> TTImp -> ITy
dataRecord : Type
Totality: total
Constructor: 
MkRecord : FC -> Name -> List (Name, (Count, (PiInfoTTImp, TTImp))) -> Name -> ListIField -> Record
dataTTImp : 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 -> ListDecl -> 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
dataUseSide : Type
Totality: total
Constructors:
UseLeft : UseSide
UseRight : UseSide
dataWithFlag : Type
Totality: total
Constructor: 
Syntactic : WithFlag
getFC : TTImp -> FC
Totality: total