Idris2Doc : Core.Context.Context

Core.Context.Context

(source)
Reexports
import public Core.Name
import public Core.Options.Log
import public Core.TT
import public Core.WithData
import public Algebra.SizeChange
Definitions
data Ref : label -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRef : IORef a -> Ref x a
data HoleInfo : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NotHole : HoleInfo
  
SolvedHole : Nat -> HoleInfo

  Hint: 
TTC HoleInfo
record PMDefInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPMDefInfo : HoleInfo -> Bool -> Bool -> PMDefInfo

  Projections:
  
.alwaysReduce : PMDefInfo -> Bool
  
.externalDecl : PMDefInfo -> Bool
  
.holeInfo : PMDefInfo -> HoleInfo

  Hint: 
TTC PMDefInfo
.holeInfo : PMDefInfo -> HoleInfo
  Visibility: public export
holeInfo : PMDefInfo -> HoleInfo
  Visibility: public export
.alwaysReduce : PMDefInfo -> Bool
  Visibility: public export
alwaysReduce : PMDefInfo -> Bool
  Visibility: public export
.externalDecl : PMDefInfo -> Bool
  Visibility: public export
externalDecl : PMDefInfo -> Bool
  Visibility: public export
defaultPI : PMDefInfo
  Visibility: export
record TypeFlags : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTypeFlags : Bool -> Bool -> TypeFlags

  Projections:
  
.external : TypeFlags -> Bool
  
.uniqueAuto : TypeFlags -> Bool

  Hint: 
TTC TypeFlags
.uniqueAuto : TypeFlags -> Bool
  Visibility: public export
uniqueAuto : TypeFlags -> Bool
  Visibility: public export
.external : TypeFlags -> Bool
  Visibility: public export
external : TypeFlags -> Bool
  Visibility: public export
defaultFlags : TypeFlags
  Visibility: export
record HoleFlags : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkHoleFlags : Bool -> Bool -> HoleFlags

  Projections:
  
.implbind : HoleFlags -> Bool
  
.precisetype : HoleFlags -> Bool
.implbind : HoleFlags -> Bool
  Visibility: public export
implbind : HoleFlags -> Bool
  Visibility: public export
.precisetype : HoleFlags -> Bool
  Visibility: public export
precisetype : HoleFlags -> Bool
  Visibility: public export
holeInit : Bool -> HoleFlags
  Visibility: export
data Def : Type
  Totality: total
  Visibility: public export
  Constructors:
  
None : Def
  
PMDef : PMDefInfo -> (args : Scope) -> CaseTree args -> CaseTree args -> List (vs : Scope ** (Env Term vs, (Term vs, Term vs))) -> Def
  
ExternDef : Nat -> Def
  
ForeignDef : Nat -> List String -> Def
  
Builtin : PrimFn arity -> Def
  
DCon : Int -> Nat -> Maybe (Bool, Nat) -> Def
  
TCon : Nat -> NatSet -> NatSet -> TypeFlags -> List Name -> Maybe (List Name) -> Maybe NatSet -> Def
  
Hole : Nat -> HoleFlags -> Def
  
BySearch : RigCount -> Nat -> Name -> Def
  
Guess : ClosedTerm -> Nat -> List Int -> Def
  
ImpBind : Def
  
UniverseLevel : Integer -> Def
  
Delayed : Def

  Hints:
  
HasNames Def
  
Show Def
  
StripNamespace Def
  
TTC Def
defNameType : Def -> Maybe NameType
  Visibility: export
Constructor' : Type -> Type
  Visibility: public export
Constructor : Type
  Visibility: public export
data DataDef : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkData : Constructor -> List Constructor -> DataDef
data Clause : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkClause : Env Term vars -> Term vars -> Term vars -> Clause

  Hints:
  
HasNames Clause
  
Show Clause
data DefFlag : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Inline : DefFlag
  
NoInline : DefFlag
  
Deprecate : DefFlag
  A definition has been marked as deprecated
  
Invertible : DefFlag
  
Overloadable : DefFlag
  
TCInline : DefFlag
  
SetTotal : TotalReq -> DefFlag
  
BlockedHint : DefFlag
  
Macro : DefFlag
  
PartialEval : List (Name, Nat) -> DefFlag
  
AllGuarded : DefFlag
  
ConType : ConInfo -> DefFlag
  
Identity : Nat -> DefFlag

  Hints:
  
Eq DefFlag
  
Show DefFlag
  
TTC DefFlag
record SCCall : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSCCall : Name -> Matrix SizeChange -> FC -> SCCall

  Projections:
  
.fnArgs : SCCall -> Matrix SizeChange
  
.fnCall : SCCall -> Name
  
.fnLoc : SCCall -> FC

  Hints:
  
Eq SCCall
  
HasNames SCCall
  
Show SCCall
  
TTC SCCall
.fnCall : SCCall -> Name
  Visibility: public export
fnCall : SCCall -> Name
  Visibility: public export
.fnArgs : SCCall -> Matrix SizeChange
  Visibility: public export
fnArgs : SCCall -> Matrix SizeChange
  Visibility: public export
.fnLoc : SCCall -> FC
  Visibility: public export
fnLoc : SCCall -> FC
  Visibility: public export
data SchemeMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
EvalAll : SchemeMode
  
BlockExport : SchemeMode

  Hint: 
Eq SchemeMode
record GlobalDef : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkGlobalDef : FC -> Name -> ClosedTerm -> NatSet -> NatSet -> NatSet -> NatSet -> RigCount -> Scope -> WithDefault Visibility Private -> Totality -> Bool -> List DefFlag -> Maybe (NameMap Bool) -> Maybe (NameMap Bool) -> Bool -> Bool -> Bool -> Def -> Maybe CDef -> Maybe NamedDef -> List SCCall -> Maybe (SchemeMode, SchemeObj Write) -> GlobalDef

  Projections:
  
.compexpr : GlobalDef -> Maybe CDef
  
.definition : GlobalDef -> Def
  
.eraseArgs : GlobalDef -> NatSet
  
.flags : GlobalDef -> List DefFlag
  
.fullname : GlobalDef -> Name
  
.inferrable : GlobalDef -> NatSet
  
.invertible : GlobalDef -> Bool
  
.isEscapeHatch : GlobalDef -> Bool
  
.linearChecked : GlobalDef -> Bool
  
.localVars : GlobalDef -> Scope
  
.location : GlobalDef -> FC
  
.multiplicity : GlobalDef -> RigCount
  
.namedcompexpr : GlobalDef -> Maybe NamedDef
  
.noCycles : GlobalDef -> Bool
  
.refersToM : GlobalDef -> Maybe (NameMap Bool)
  
.refersToRuntimeM : GlobalDef -> Maybe (NameMap Bool)
  
.safeErase : GlobalDef -> NatSet
  
.schemeExpr : GlobalDef -> Maybe (SchemeMode, SchemeObj Write)
  
.sizeChange : GlobalDef -> List SCCall
  
.specArgs : GlobalDef -> NatSet
  
.totality : GlobalDef -> Totality
  
.type : GlobalDef -> ClosedTerm
  
.visibility : GlobalDef -> WithDefault Visibility Private

  Hints:
  
HasNames GlobalDef
  
StripNamespace GlobalDef
  
TTC GlobalDef
.location : GlobalDef -> FC
  Visibility: public export
location : GlobalDef -> FC
  Visibility: public export
.fullname : GlobalDef -> Name
  Visibility: public export
fullname : GlobalDef -> Name
  Visibility: public export
.type : GlobalDef -> ClosedTerm
  Visibility: public export
type : GlobalDef -> ClosedTerm
  Visibility: public export
.eraseArgs : GlobalDef -> NatSet
  Visibility: public export
eraseArgs : GlobalDef -> NatSet
  Visibility: public export
.safeErase : GlobalDef -> NatSet
  Visibility: public export
safeErase : GlobalDef -> NatSet
  Visibility: public export
.specArgs : GlobalDef -> NatSet
  Visibility: public export
specArgs : GlobalDef -> NatSet
  Visibility: public export
.inferrable : GlobalDef -> NatSet
  Visibility: public export
inferrable : GlobalDef -> NatSet
  Visibility: public export
.multiplicity : GlobalDef -> RigCount
  Visibility: public export
multiplicity : GlobalDef -> RigCount
  Visibility: public export
.localVars : GlobalDef -> Scope
  Visibility: public export
localVars : GlobalDef -> Scope
  Visibility: public export
.visibility : GlobalDef -> WithDefault Visibility Private
  Visibility: public export
visibility : GlobalDef -> WithDefault Visibility Private
  Visibility: public export
.totality : GlobalDef -> Totality
  Visibility: public export
totality : GlobalDef -> Totality
  Visibility: public export
.isEscapeHatch : GlobalDef -> Bool
  Visibility: public export
isEscapeHatch : GlobalDef -> Bool
  Visibility: public export
.flags : GlobalDef -> List DefFlag
  Visibility: public export
flags : GlobalDef -> List DefFlag
  Visibility: public export
.refersToM : GlobalDef -> Maybe (NameMap Bool)
  Visibility: public export
refersToM : GlobalDef -> Maybe (NameMap Bool)
  Visibility: public export
.refersToRuntimeM : GlobalDef -> Maybe (NameMap Bool)
  Visibility: public export
refersToRuntimeM : GlobalDef -> Maybe (NameMap Bool)
  Visibility: public export
.invertible : GlobalDef -> Bool
  Visibility: public export
invertible : GlobalDef -> Bool
  Visibility: public export
.noCycles : GlobalDef -> Bool
  Visibility: public export
noCycles : GlobalDef -> Bool
  Visibility: public export
.linearChecked : GlobalDef -> Bool
  Visibility: public export
linearChecked : GlobalDef -> Bool
  Visibility: public export
.definition : GlobalDef -> Def
  Visibility: public export
definition : GlobalDef -> Def
  Visibility: public export
.compexpr : GlobalDef -> Maybe CDef
  Visibility: public export
compexpr : GlobalDef -> Maybe CDef
  Visibility: public export
.namedcompexpr : GlobalDef -> Maybe NamedDef
  Visibility: public export
namedcompexpr : GlobalDef -> Maybe NamedDef
  Visibility: public export
.sizeChange : GlobalDef -> List SCCall
  Visibility: public export
sizeChange : GlobalDef -> List SCCall
  Visibility: public export
.schemeExpr : GlobalDef -> Maybe (SchemeMode, SchemeObj Write)
  Visibility: public export
schemeExpr : GlobalDef -> Maybe (SchemeMode, SchemeObj Write)
  Visibility: public export
getDefNameType : GlobalDef -> NameType
  Visibility: export
gDefKindedName : GlobalDef -> KindedName
  Visibility: export
refersTo : GlobalDef -> NameMap Bool
  Visibility: export
refersToRuntime : GlobalDef -> NameMap Bool
  Visibility: export
findSetTotal : List DefFlag -> Maybe TotalReq
  Visibility: export
data Arr : Type
  Totality: total
  Visibility: export
data ContextEntry : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Coded : Namespace -> Binary -> ContextEntry
  
Decoded : GlobalDef -> ContextEntry
data PossibleName : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Direct : Name -> Int -> PossibleName
  
Alias : Name -> Name -> Int -> PossibleName
data UConstraint : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ULE : Name -> Name -> UConstraint
  
ULT : Name -> Name -> UConstraint

  Hints:
  
Eq UConstraint
  
HasNames UConstraint
  
Ord UConstraint
record Context : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkContext : Int -> Int -> NameMap Int -> UserNameMap (List PossibleName) -> Ref Arr (IOArray ContextEntry) -> Nat -> IntMap ContextEntry -> List Namespace -> Bool -> Bool -> NameMap () -> List UConstraint -> Context

  Projections:
  
.allPublic : Context -> Bool
  
.branchDepth : Context -> Nat
  
.content : Context -> Ref Arr (IOArray ContextEntry)
  
.firstEntry : Context -> Int
  
.hidden : Context -> NameMap ()
  
.inlineOnly : Context -> Bool
  
.nextEntry : Context -> Int
  
.possibles : Context -> UserNameMap (List PossibleName)
  
.resolvedAs : Context -> NameMap Int
  
.staging : Context -> IntMap ContextEntry
  
.uconstraints : Context -> List UConstraint
  
.visibleNS : Context -> List Namespace
.firstEntry : Context -> Int
  Visibility: public export
firstEntry : Context -> Int
  Visibility: public export
.nextEntry : Context -> Int
  Visibility: public export
nextEntry : Context -> Int
  Visibility: public export
.resolvedAs : Context -> NameMap Int
  Visibility: public export
resolvedAs : Context -> NameMap Int
  Visibility: public export
.possibles : Context -> UserNameMap (List PossibleName)
  Visibility: public export
possibles : Context -> UserNameMap (List PossibleName)
  Visibility: public export
.content : Context -> Ref Arr (IOArray ContextEntry)
  Visibility: public export
content : Context -> Ref Arr (IOArray ContextEntry)
  Visibility: public export
.branchDepth : Context -> Nat
  Visibility: public export
branchDepth : Context -> Nat
  Visibility: public export
.staging : Context -> IntMap ContextEntry
  Visibility: public export
staging : Context -> IntMap ContextEntry
  Visibility: public export
.visibleNS : Context -> List Namespace
  Visibility: public export
visibleNS : Context -> List Namespace
  Visibility: public export
.allPublic : Context -> Bool
  Visibility: public export
allPublic : Context -> Bool
  Visibility: public export
.inlineOnly : Context -> Bool
  Visibility: public export
inlineOnly : Context -> Bool
  Visibility: public export
.hidden : Context -> NameMap ()
  Visibility: public export
hidden : Context -> NameMap ()
  Visibility: public export
.uconstraints : Context -> List UConstraint
  Visibility: public export
uconstraints : Context -> List UConstraint
  Visibility: public export