Core.TT

Reexports

Definitions

record KindedName : Type

Totality: total
Visibility: public export
Constructor: 

MkKindedName : Maybe NameType -> Name -> Name -> KindedName

Projections:

.fullName : KindedName -> Name

.nameKind : KindedName -> Maybe NameType

.rawName : KindedName -> Name

Hints:

Pretty IdrisSyntax (BasicMultiBinder' KindedName)

Pretty IdrisSyntax (PBinder' KindedName)

Show KindedName

.nameKind : KindedName -> Maybe NameType

Visibility: public export

nameKind : KindedName -> Maybe NameType

Visibility: public export

.fullName : KindedName -> Name

Visibility: public export

fullName : KindedName -> Name

Visibility: public export

.rawName : KindedName -> Name

Visibility: public export

rawName : KindedName -> Name

Visibility: public export

defaultKindedName : Name -> KindedName

Visibility: export

funKindedName : Name -> KindedName

Visibility: export

data CList : List a -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : CList [] ty

(::) : ty -> CList cs ty -> CList (c :: cs) ty

data Visibility : Type

Totality: total
Visibility: public export
Constructors:

Private : Visibility

Export : Visibility

Public : Visibility

Hints:

Eq Visibility

Ord Visibility

Pretty Void Visibility

Reflect Visibility

Reify Visibility

Show Visibility

TTC Visibility

data DataOpt : Type

Totality: total
Visibility: public export
Constructors:

SearchBy : List1 Name -> DataOpt

NoHints : DataOpt

UniqueSearch : DataOpt

External : DataOpt

NoNewtype : DataOpt

Hint: 

Eq DataOpt

data Fixity : Type

Totality: total
Visibility: public export
Constructors:

InfixL : Fixity

InfixR : Fixity

Infix : Fixity

Prefix : Fixity

Hints:

Eq Fixity

Interpolation Fixity

Show Fixity

data BindingModifier : Type

Totality: total
Visibility: public export
Constructors:

NotBinding : BindingModifier

Autobind : BindingModifier

Typebind : BindingModifier

Hints:

Eq BindingModifier

HasDefault BindingModifier

Interpolation BindingModifier

Show BindingModifier

record FixityInfo : Type

Totality: total
Visibility: public export
Constructor: 

MkFixityInfo : FC -> Visibility -> BindingModifier -> Fixity -> Nat -> FixityInfo

Projections:

.bindingInfo : FixityInfo -> BindingModifier

.fc : FixityInfo -> FC

.fix : FixityInfo -> Fixity

.precedence : FixityInfo -> Nat

.vis : FixityInfo -> Visibility

Hints:

Eq FixityInfo

Show FixityInfo

.fc : FixityInfo -> FC

Visibility: public export

fc : FixityInfo -> FC

Visibility: public export

.vis : FixityInfo -> Visibility

Visibility: public export

vis : FixityInfo -> Visibility

Visibility: public export

.bindingInfo : FixityInfo -> BindingModifier

Visibility: public export

bindingInfo : FixityInfo -> BindingModifier

Visibility: public export

.fix : FixityInfo -> Fixity

Visibility: public export

fix : FixityInfo -> Fixity

Visibility: public export

.precedence : FixityInfo -> Nat

Visibility: public export

precedence : FixityInfo -> Nat

Visibility: public export

data FixityDeclarationInfo : Type

  Whenever we read an operator from the parser, we don't know if it's a backticked expression with no fixity
  declaration, or if it has a fixity declaration. If it does not have a declaration, we represent this state
  with `UndeclaredFixity`.
  Note that a backticked expression can have a fixity declaration, in which case it is represented with
  `DeclaredFixity`.

Totality: total
Visibility: public export
Constructors:

UndeclaredFixity : FixityDeclarationInfo

DeclaredFixity : FixityInfo -> FixityDeclarationInfo

data OperatorLHSInfo : tm -> Type

Totality: total
Visibility: public export
Constructors:

NoBinder : tm -> OperatorLHSInfo tm

BindType : tm -> tm -> OperatorLHSInfo tm

BindExpr : tm -> tm -> OperatorLHSInfo tm

BindExplicitType : tm -> tm -> tm -> OperatorLHSInfo tm

Hints:

Functor OperatorLHSInfo

Show (OperatorLHSInfo tm)

.getLhs : OperatorLHSInfo tm -> tm

Visibility: export

.getBoundPat : OperatorLHSInfo tm -> Maybe tm

Visibility: export

.getBinder : OperatorLHSInfo tm -> BindingModifier

Visibility: export

data TotalReq : Type

Totality: total
Visibility: public export
Constructors:

Total : TotalReq

CoveringOnly : TotalReq

PartialOK : TotalReq

Hints:

Eq TotalReq

Ord TotalReq

Reflect TotalReq

Reify TotalReq

Show TotalReq

TTC TotalReq

data PartialReason : Type

Totality: total
Visibility: public export
Constructors:

NotStrictlyPositive : PartialReason

BadCall : List Name -> PartialReason

BadPath : List (FC, Name) -> Name -> PartialReason

RecPath : List (FC, Name) -> PartialReason

Hints:

HasNames PartialReason

Pretty Void PartialReason

Show PartialReason

TTC PartialReason

data Terminating : Type

Totality: total
Visibility: public export
Constructors:

Unchecked : Terminating

IsTerminating : Terminating

NotTerminating : PartialReason -> Terminating

Hints:

HasNames Terminating

Pretty Void Terminating

Show Terminating

TTC Terminating

data Covering : Type

Totality: total
Visibility: public export
Constructors:

IsCovering : Covering

MissingCases : List ClosedTerm -> Covering

NonCoveringCall : List Name -> Covering

Hints:

HasNames Covering

Pretty Void Covering

Show Covering

TTC Covering

record Totality : Type

Totality: total
Visibility: public export
Constructor: 

MkTotality : Terminating -> Covering -> Totality

Projections:

.isCovering : Totality -> Covering

.isTerminating : Totality -> Terminating

Hints:

HasNames Totality

Pretty Void Totality

Show Totality

TTC Totality

.isTerminating : Totality -> Terminating

Visibility: public export

isTerminating : Totality -> Terminating

Visibility: public export

.isCovering : Totality -> Covering

Visibility: public export

isCovering : Totality -> Covering

Visibility: public export

unchecked : Totality

Visibility: export

isTotal : Totality

Visibility: export

notCovering : Totality

Visibility: export

data Bounds : Scoped

Totality: total
Visibility: public export
Constructors:

None : Bounds empty

Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)

sizeOf : Bounds xs -> SizeOf xs

Visibility: export

addVars : SizeOf outer -> Bounds bound -> NVar name (outer ++ vars) -> NVar name (outer ++ (bound ++ vars))

Visibility: export

resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name -> Maybe (Var (outer ++ (done <>> (bound ++ vars))))

Visibility: export

refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)

Visibility: export

refToLocal : Name -> (new : Name) -> Term vars -> Term (new :: vars)

Visibility: export

substName : Name -> Term vars -> Term vars -> Term vars

Visibility: export

addMetas : Bool -> NameMap Bool -> Term vars -> NameMap Bool

Visibility: export

getMetas : Term vars -> NameMap Bool

Visibility: export

addRefs : Bool -> Name -> NameMap Bool -> Term vars -> NameMap Bool

Visibility: export

getRefs : Name -> Term vars -> NameMap Bool

Visibility: export