Idris2Doc : Language.Reflection.TTImp

Language.Reflection.TTImp

data AltType : Type
  Totality: total
  Constructors:
  
FirstSuccess : AltType
  
Unique : AltType
  
UniqueDefault : TTImp -> AltType
data BindMode : Type
  Totality: total
  Constructors:
  
PI : Count -> BindMode
  
PATTERN : BindMode
  
NONE : BindMode
data Clause : Type
  Totality: total
  Constructors:
  
PatClause : FC -> TTImp -> TTImp -> Clause
  
WithClause : FC -> TTImp -> TTImp -> Maybe Name -> List WithFlag -> List Clause -> Clause
  
ImpossibleClause : FC -> TTImp -> Clause
data Data : Type
  Totality: total
  Constructors:
  
MkData : FC -> Name -> TTImp -> List DataOpt -> List ITy -> Data
  
MkLater : FC -> Name -> TTImp -> Data
data DataOpt : Type
  Totality: total
  Constructors:
  
SearchBy : List Name -> DataOpt
  
NoHints : DataOpt
  
UniqueSearch : DataOpt
  
External : DataOpt
  
NoNewtype : DataOpt
data Decl : Type
  Totality: total
  Constructors:
  
IClaim : FC -> Count -> Visibility -> List FnOpt -> ITy -> Decl
  
IData : FC -> Visibility -> Data -> Decl
  
IDef : FC -> Name -> List Clause -> Decl
  
IParameters : FC -> List (Name, (Count, (PiInfo TTImp, TTImp))) -> List Decl -> Decl
  
IRecord : FC -> Maybe String -> Visibility -> Record -> Decl
  
INamespace : FC -> Namespace -> List Decl -> Decl
  
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
  
IRunElabDecl : FC -> TTImp -> Decl
  
ILog : Maybe (List String, Nat) -> Decl
  
IBuiltin : FC -> BuiltinType -> Name -> Decl
data DotReason : Type
  Totality: total
  Constructors:
  
NonLinearVar : DotReason
  
VarApplied : DotReason
  
NotConstructor : DotReason
  
ErasedArg : DotReason
  
UserDotted : DotReason
  
UnknownDot : DotReason
  
UnderAppliedCon : DotReason
data FnOpt : Type
  Totality: total
  Constructors:
  
Inline : FnOpt
  
TCInline : FnOpt
  
Hint : Bool -> FnOpt
  
GlobalHint : Bool -> FnOpt
  
ExternFn : FnOpt
  
ForeignFn : List TTImp -> FnOpt
  
Invertible : FnOpt
  
Totality : TotalReq -> FnOpt
  
Macro : FnOpt
  
SpecArgs : List Name -> FnOpt
data IField : Type
  Totality: total
  Constructor: 
MkIField : FC -> Count -> PiInfo TTImp -> Name -> TTImp -> IField
data IFieldUpdate : Type
  Totality: total
  Constructors:
  
ISetField : List String -> TTImp -> IFieldUpdate
  
ISetFieldApp : List String -> TTImp -> IFieldUpdate
data ITy : Type
  Totality: total
  Constructor: 
MkTy : FC -> FC -> Name -> TTImp -> ITy
data Record : Type
  Totality: total
  Constructor: 
MkRecord : FC -> Name -> List (Name, (Count, (PiInfo TTImp, TTImp))) -> Name -> List IField -> Record
data TTImp : Type
  Totality: total
  Constructors:
  
IVar : FC -> Name -> TTImp
  
IPi : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp
  
ILam : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp
  
ILet : FC -> FC -> Count -> Name -> TTImp -> TTImp -> TTImp -> TTImp
  
ICase : FC -> TTImp -> TTImp -> List Clause -> TTImp
  
ILocal : FC -> List Decl -> TTImp -> TTImp
  
IUpdate : FC -> List IFieldUpdate -> 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 -> List TTImp -> 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 -> List Decl -> TTImp
  
IUnquote : FC -> TTImp -> TTImp
  
IPrimVal : FC -> Constant -> TTImp
  
IType : FC -> TTImp
  
IHole : FC -> String -> TTImp
  
Implicit : FC -> Bool -> TTImp
  
IWithUnambigNames : FC -> List Name -> TTImp -> TTImp
data UseSide : Type
  Totality: total
  Constructors:
  
UseLeft : UseSide
  
UseRight : UseSide
data WithFlag : Type
  Totality: total
  Constructor: 
Syntactic : WithFlag
getFC : TTImp -> FC
  Totality: total