Idris2Doc : Core.Context

Core.Context

(source)
Reexports
import public Core.Context.Context
import public Core.Core
import public Core.Name
import public Core.Options.Log
import public Core.TT
Definitions
getContent : Context -> Ref Arr (IOArray ContextEntry)
  Visibility: export
namesResolvedAs : Context -> NameMap Name
  Visibility: export
decode : Context -> Int -> Bool -> ContextEntry -> Core GlobalDef
  Visibility: export
initCtxtS : Int -> Core Context
  Visibility: export
initCtxt : Core Context
  Visibility: export
newEntry : Name -> Context -> Core (Int, Context)
  Visibility: export
getPosition : Name -> Context -> Core (Int, Context)
  Visibility: export
getNameID : Name -> Context -> Maybe Int
  Visibility: export
addCtxt : Name -> GlobalDef -> Context -> Core (Int, Context)
  Visibility: export
addEntry : Name -> ContextEntry -> Context -> Core (Int, Context)
  Visibility: export
lookupCtxtExactI : Name -> Context -> Core (Maybe (Int, GlobalDef))
  Visibility: export
lookupCtxtExact : Name -> Context -> Core (Maybe GlobalDef)
  Visibility: export
lookupContextEntry : Name -> Context -> Core (Maybe (Int, ContextEntry))
  Visibility: export
isHidden : Name -> Context -> Bool
  Check if the given name has been hidden by the `%hide` directive.

  Visibility: export
lookupCtxtName' : Bool -> Name -> Context -> Core (List (Name, (Int, GlobalDef)))
  Look up a possibly hidden name in the context. The first (boolean) argument
  controls whether names hidden by `%hide` are returned too (True=yes, False=no).

  Visibility: export
lookupCtxtName : Name -> Context -> Core (List (Name, (Int, GlobalDef)))
  Look up a name in the context, ignoring names hidden by `%hide`.

  Visibility: export
lookupHiddenCtxtName : Name -> Context -> Core (List (Name, (Int, GlobalDef)))
  Look up a (possible hidden) name in the context.

  Visibility: export
newDef : FC -> Name -> RigCount -> Scope -> ClosedTerm -> WithDefault Visibility Private -> Def -> GlobalDef
  Produce a new global definition with a lot of default values
  @fc   definition site
  @n    name
  @rig  quantity annotation
  @vars local variables
  @ty   (closed) type
  @vis  Visibility, defaulting to private
  @def  actual definition

  Visibility: export
data Transform : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTransform : Name -> Env Term vars -> Term vars -> Term vars -> Transform

  Hints:
  
HasNames (Name, Transform)
  
HasNames Transform
  
TTC Transform
data BuiltinType : Type
  Types that are transformed into a faster representation
  during codegen.

  Totality: total
  Visibility: public export
  Constructors:
  
BuiltinNatural : BuiltinType
  
NaturalToInteger : BuiltinType
  
IntegerToNatural : BuiltinType

  Hint: 
Show BuiltinType
getFnName : Transform -> Maybe Name
  Visibility: export
interface HasNames : Type -> Type
  Parameters: a
Methods:
  
full : Context -> a -> Core a
  
resolved : Context -> a -> Core a

Implementations:
  
HasNames (ArgType vars)
  
HasNames (PatInfo n vars)
  
HasNames (NamedPats todo vars)
  
HasNames (PatClause todo vars)
  
HasNames Metadata
  
HasNames a => HasNames (List a)
  
HasNames (Int, (FC, Name))
  
HasNames (Name, Bool)
  
HasNames (Name, List a)
  
HasNames (Name, Transform)
  
HasNames (Name, (Name, Bool))
  
HasNames e => HasNames (TTCFile e)
  
HasNames (NHead free)
  
HasNames (NF free)
  
HasNames IFaceInfo
  
HasNames a => HasNames (ANameMap a)
  
HasNames SyntaxInfo
  
HasNames Name
  
HasNames UConstraint
  
HasNames (Term vars)
  
HasNames Pat
  
HasNames (CaseTree vars)
  
HasNames (CaseAlt vars)
  
HasNames (Env Term vars)
  
HasNames Clause
  
HasNames Def
  
HasNames (NameMap a)
  
HasNames PartialReason
  
HasNames Terminating
  
HasNames Covering
  
HasNames CaseError
  
HasNames Warning
  
HasNames Error
  
HasNames Totality
  
HasNames SCCall
  
HasNames a => HasNames (Maybe a)
  
HasNames GlobalDef
  
HasNames Transform
full : HasNames a => Context -> a -> Core a
  Visibility: public export
resolved : HasNames a => Context -> a -> Core a
  Visibility: public export
allNames : Context -> Core (List Name)
  Visibility: export
record Defs : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDefs : Context -> List Name -> Namespace -> List Namespace -> Options -> NameMap () -> NameMap (List (Name, Bool)) -> NameMap Bool -> NameMap () -> NameMap () -> List (Name, (Name, Bool)) -> List (Name, Bool) -> NameMap (List Transform) -> List (Name, Transform) -> NameMap (List String) -> Int -> List (Namespace, Int) -> List (ModuleIdent, (Bool, Namespace)) -> List (String, (ModuleIdent, (Bool, Namespace))) -> List (CG, String) -> List Name -> List (CG, (String, List String)) -> List (CG, (List String, List String)) -> NameMap () -> NameMap Bool -> NameMap () -> StringMap (Bool, Integer) -> Maybe (Integer, String) -> List Warning -> Bool -> NameMap (List (String, String)) -> SnocList Name -> Defs

  Projections:
  
.allImported : Defs -> List (String, (ModuleIdent, (Bool, Namespace)))
  
.allIncData : Defs -> List (CG, (List String, List String))
  
.autoHints : Defs -> NameMap Bool
  
.cgdirectives : Defs -> List (CG, String)
  
.currentNS : Defs -> Namespace
  
.defsStack : Defs -> SnocList Name
  
.foreignExports : Defs -> NameMap (List (String, String))
  
.gamma : Defs -> Context
  
.ifaceHash : Defs -> Int
  
.importHashes : Defs -> List (Namespace, Int)
  
.imported : Defs -> List (ModuleIdent, (Bool, Namespace))
  
.incData : Defs -> List (CG, (String, List String))
  
.localHints : Defs -> NameMap ()
  
.mutData : Defs -> List Name
  
.namedirectives : Defs -> NameMap (List String)
  
.nestedNS : Defs -> List Namespace
  
.openHints : Defs -> NameMap ()
  
.options : Defs -> Options
  
.peFailures : Defs -> NameMap ()
  
.saveAutoHints : Defs -> List (Name, Bool)
  
.saveTransforms : Defs -> List (Name, Transform)
  
.saveTypeHints : Defs -> List (Name, (Name, Bool))
  
.schemeEvalLoaded : Defs -> Bool
  
.timer : Defs -> Maybe (Integer, String)
  
.timings : Defs -> StringMap (Bool, Integer)
  
.toCompileCase : Defs -> List Name
  
.toIR : Defs -> NameMap ()
  
.toSave : Defs -> NameMap ()
  
.transforms : Defs -> NameMap (List Transform)
  
.typeHints : Defs -> NameMap (List (Name, Bool))
  
.userHoles : Defs -> NameMap Bool
  
.warnings : Defs -> List Warning
.gamma : Defs -> Context
  Visibility: public export
gamma : Defs -> Context
  Visibility: public export
.mutData : Defs -> List Name
  Visibility: public export
mutData : Defs -> List Name
  Visibility: public export
.currentNS : Defs -> Namespace
  Visibility: public export
currentNS : Defs -> Namespace
  Visibility: public export
.nestedNS : Defs -> List Namespace
  Visibility: public export
nestedNS : Defs -> List Namespace
  Visibility: public export
.options : Defs -> Options
  Visibility: public export
options : Defs -> Options
  Visibility: public export
.toSave : Defs -> NameMap ()
  Visibility: public export
toSave : Defs -> NameMap ()
  Visibility: public export
.typeHints : Defs -> NameMap (List (Name, Bool))
  Visibility: public export
typeHints : Defs -> NameMap (List (Name, Bool))
  Visibility: public export
.autoHints : Defs -> NameMap Bool
  Visibility: public export
autoHints : Defs -> NameMap Bool
  Visibility: public export
.openHints : Defs -> NameMap ()
  Visibility: public export
openHints : Defs -> NameMap ()
  Visibility: public export
.localHints : Defs -> NameMap ()
  Visibility: public export
localHints : Defs -> NameMap ()
  Visibility: public export
.saveTypeHints : Defs -> List (Name, (Name, Bool))
  Visibility: public export
saveTypeHints : Defs -> List (Name, (Name, Bool))
  Visibility: public export
.saveAutoHints : Defs -> List (Name, Bool)
  Visibility: public export
saveAutoHints : Defs -> List (Name, Bool)
  Visibility: public export
.transforms : Defs -> NameMap (List Transform)
  Visibility: public export
transforms : Defs -> NameMap (List Transform)
  Visibility: public export
.saveTransforms : Defs -> List (Name, Transform)
  Visibility: public export
saveTransforms : Defs -> List (Name, Transform)
  Visibility: public export
.namedirectives : Defs -> NameMap (List String)
  Visibility: public export
namedirectives : Defs -> NameMap (List String)
  Visibility: public export
.ifaceHash : Defs -> Int
  Visibility: public export
ifaceHash : Defs -> Int
  Visibility: public export
.importHashes : Defs -> List (Namespace, Int)
  Visibility: public export
importHashes : Defs -> List (Namespace, Int)
  Visibility: public export
.imported : Defs -> List (ModuleIdent, (Bool, Namespace))
  Visibility: public export
imported : Defs -> List (ModuleIdent, (Bool, Namespace))
  Visibility: public export
.allImported : Defs -> List (String, (ModuleIdent, (Bool, Namespace)))
  Visibility: public export
allImported : Defs -> List (String, (ModuleIdent, (Bool, Namespace)))
  Visibility: public export
.cgdirectives : Defs -> List (CG, String)
  Visibility: public export
cgdirectives : Defs -> List (CG, String)
  Visibility: public export
.toCompileCase : Defs -> List Name
  Visibility: public export
toCompileCase : Defs -> List Name
  Visibility: public export
.incData : Defs -> List (CG, (String, List String))
  Visibility: public export
incData : Defs -> List (CG, (String, List String))
  Visibility: public export
.allIncData : Defs -> List (CG, (List String, List String))
  Visibility: public export
allIncData : Defs -> List (CG, (List String, List String))
  Visibility: public export
.toIR : Defs -> NameMap ()
  Visibility: public export
toIR : Defs -> NameMap ()
  Visibility: public export
.userHoles : Defs -> NameMap Bool
  Visibility: public export
userHoles : Defs -> NameMap Bool
  Visibility: public export
.peFailures : Defs -> NameMap ()
  Visibility: public export
peFailures : Defs -> NameMap ()
  Visibility: public export
.timings : Defs -> StringMap (Bool, Integer)
  Visibility: public export
timings : Defs -> StringMap (Bool, Integer)
  Visibility: public export
.timer : Defs -> Maybe (Integer, String)
  Visibility: public export
timer : Defs -> Maybe (Integer, String)
  Visibility: public export
.warnings : Defs -> List Warning
  Visibility: public export
warnings : Defs -> List Warning
  Visibility: public export
.schemeEvalLoaded : Defs -> Bool
  Visibility: public export
schemeEvalLoaded : Defs -> Bool
  Visibility: public export
.foreignExports : Defs -> NameMap (List (String, String))
  Visibility: public export
foreignExports : Defs -> NameMap (List (String, String))
  Visibility: public export
.defsStack : Defs -> SnocList Name
  Visibility: public export
defsStack : Defs -> SnocList Name
  Visibility: public export
data Ctxt : Type
  Totality: total
  Visibility: export
clearDefs : Defs -> Core Defs
  Visibility: export
initDefs : Core Defs
  Visibility: export
clearCtxt : Ref Ctxt Defs => Core ()
  Visibility: export
getFieldNames : Context -> Namespace -> List Name
  Visibility: export
getSimilarNames : Ref Ctxt Defs => {default Nothing _ : Maybe ((Name, GlobalDef) -> Core Bool)} -> Name -> Core (Maybe (String, List (Name, (Visibility, Nat))))
  Visibility: export
showSimilarNames : Namespace -> Name -> String -> List (Name, (Visibility, Nat)) -> List String
  Visibility: export
undefinedName : Ref Ctxt Defs => FC -> Name -> Core a
  Visibility: export
noDeclaration : Ref Ctxt Defs => FC -> Name -> Core a
  Visibility: export
ambiguousName : Ref Ctxt Defs => FC -> Name -> List Name -> Core a
  Visibility: export
canonicalName : Ref Ctxt Defs => FC -> Name -> Core Name
  Visibility: export
aliasName : Ref Ctxt Defs => Name -> Core Name
  Visibility: export
addHash : Ref Ctxt Defs => Hashable a => a -> Core ()
  Visibility: export
initHash : Ref Ctxt Defs => Core ()
  Visibility: export
addUserHole : Ref Ctxt Defs => Bool -> Name -> Core ()
  Visibility: export
clearUserHole : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
getUserHoles : Ref Ctxt Defs => Core (List Name)
  Visibility: export
addDef : Ref Ctxt Defs => Name -> GlobalDef -> Core Int
  Visibility: export
addContextEntry : Ref Ctxt Defs => Namespace -> Name -> Binary -> Core Int
  Visibility: export
addContextAlias : Ref Ctxt Defs => Name -> Name -> Core ()
  Visibility: export
addBuiltin : Ref Ctxt Defs => Name -> ClosedTerm -> Totality -> PrimFn arity -> Core ()
  Visibility: export
updateDef : Ref Ctxt Defs => Name -> (Def -> Maybe Def) -> Core ()
  Visibility: export
updateTy : Ref Ctxt Defs => Int -> ClosedTerm -> Core ()
  Visibility: export
setCompiled : Ref Ctxt Defs => Name -> CDef -> Core ()
  Visibility: export
setLinearCheck : Ref Ctxt Defs => Int -> Bool -> Core ()
  Visibility: export
setCtxt : Ref Ctxt Defs => Context -> Core ()
  Visibility: export
resolveName : Ref Ctxt Defs => Name -> Core Int
  Visibility: export
addName : Ref Ctxt Defs => Name -> Core Int
  Visibility: export
branch : Ref Ctxt Defs => Core Defs
  Visibility: export
commit : Ref Ctxt Defs => Core ()
  Visibility: export
depth : Ref Ctxt Defs => Core Nat
  Visibility: export
dumpStaging : Ref Ctxt Defs => Core ()
  Visibility: export
addToSave : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
lookupExactBy : (GlobalDef -> a) -> Name -> Context -> Core (Maybe a)
  Visibility: export
lookupNameBy : (GlobalDef -> a) -> Name -> Context -> Core (List (Name, (Int, a)))
  Visibility: export
lookupDefExact : Name -> Context -> Core (Maybe Def)
  Visibility: export
lookupDefName : Name -> Context -> Core (List (Name, (Int, Def)))
  Visibility: export
lookupTyExact : Name -> Context -> Core (Maybe ClosedTerm)
  Visibility: export
lookupTyName : Name -> Context -> Core (List (Name, (Int, ClosedTerm)))
  Visibility: export
lookupDefTyExact : Name -> Context -> Core (Maybe (Def, ClosedTerm))
  Visibility: export
visibleIn : Namespace -> Name -> Visibility -> Bool
  Visibility: export
visibleInAny : List Namespace -> Name -> Visibility -> Bool
  Visibility: export
reducibleInAny : List Namespace -> Name -> Visibility -> Bool
  Visibility: export
toFullNames : Ref Ctxt Defs => HasNames a => a -> Core a
  Visibility: export
toResolvedNames : Ref Ctxt Defs => HasNames a => a -> Core a
  Visibility: export
prettyName : Ref Ctxt Defs => Name -> Core String
  Visibility: export
addHashWithNames : Ref Ctxt Defs => Hashable a => HasNames a => a -> Core ()
  Visibility: export
setIsEscapeHatch : Ref Ctxt Defs => FC -> Name -> Core ()
  Visibility: export
setFlag : Ref Ctxt Defs => FC -> Name -> DefFlag -> Core ()
  Visibility: export
setNameFlag : Ref Ctxt Defs => FC -> Name -> DefFlag -> Core ()
  Visibility: export
unsetFlag : Ref Ctxt Defs => FC -> Name -> DefFlag -> Core ()
  Visibility: export
hasFlag : Ref Ctxt Defs => FC -> Name -> DefFlag -> Core Bool
  Visibility: export
hasSetTotal : Ref Ctxt Defs => FC -> Name -> Core Bool
  Visibility: export
setSizeChange : Ref Ctxt Defs => FC -> Name -> List SCCall -> Core ()
  Visibility: export
setTotality : Ref Ctxt Defs => FC -> Name -> Totality -> Core ()
  Visibility: export
setCovering : Ref Ctxt Defs => FC -> Name -> Covering -> Core ()
  Visibility: export
setTerminating : Ref Ctxt Defs => FC -> Name -> Terminating -> Core ()
  Visibility: export
getTotality : Ref Ctxt Defs => FC -> Name -> Core Totality
  Visibility: export
getSizeChange : Ref Ctxt Defs => FC -> Name -> Core (List SCCall)
  Visibility: export
setVisibility : Ref Ctxt Defs => FC -> Name -> Visibility -> Core ()
  Visibility: export
withDefStacked : Ref Ctxt Defs => Name -> Core a -> Core a
  Visibility: export
record SearchData : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSearchData : NatSet -> List (Bool, List Name) -> SearchData

  Projections:
  
.detArgs : SearchData -> NatSet
  determining argument positions
  
.hintGroups : SearchData -> List (Bool, List Name)
  Name of functions to use as hints, and whether ambiguity is allowed
  
  In proof search, for every group of names
   * If exactly one succeeds, use it
   * If more than one succeeds, report an ambiguity error
   * If none succeed, move on to the next group
  
  This allows us to prioritise some names (e.g. to declare 'open' hints,
  which we might us to open an implementation working as a module, or to
  declare a named implementation to be used globally), and to have names
  which are only used if all else fails (e.g. as a defaulting mechanism),
  while the proof search mechanism doesn't need to know about any of the
  details.
.detArgs : SearchData -> NatSet
  determining argument positions

  Visibility: public export
detArgs : SearchData -> NatSet
  determining argument positions

  Visibility: public export
.hintGroups : SearchData -> List (Bool, List Name)
  Name of functions to use as hints, and whether ambiguity is allowed
  
  In proof search, for every group of names
   * If exactly one succeeds, use it
   * If more than one succeeds, report an ambiguity error
   * If none succeed, move on to the next group
  
  This allows us to prioritise some names (e.g. to declare 'open' hints,
  which we might us to open an implementation working as a module, or to
  declare a named implementation to be used globally), and to have names
  which are only used if all else fails (e.g. as a defaulting mechanism),
  while the proof search mechanism doesn't need to know about any of the
  details.

  Visibility: public export
hintGroups : SearchData -> List (Bool, List Name)
  Name of functions to use as hints, and whether ambiguity is allowed
  
  In proof search, for every group of names
   * If exactly one succeeds, use it
   * If more than one succeeds, report an ambiguity error
   * If none succeed, move on to the next group
  
  This allows us to prioritise some names (e.g. to declare 'open' hints,
  which we might us to open an implementation working as a module, or to
  declare a named implementation to be used globally), and to have names
  which are only used if all else fails (e.g. as a defaulting mechanism),
  while the proof search mechanism doesn't need to know about any of the
  details.

  Visibility: public export
getSearchData : Ref Ctxt Defs => FC -> Bool -> Name -> Core SearchData
  Get the auto search data for a name.

  Visibility: export
setMutWith : Ref Ctxt Defs => FC -> Name -> List Name -> Core ()
  Visibility: export
addMutData : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
dropMutData : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setDetermining : Ref Ctxt Defs => FC -> Name -> List1 Name -> Core ()
  Visibility: export
setDetags : Ref Ctxt Defs => FC -> Name -> Maybe NatSet -> Core ()
  Visibility: export
setUniqueSearch : Ref Ctxt Defs => FC -> Name -> Bool -> Core ()
  Visibility: export
setExternal : Ref Ctxt Defs => FC -> Name -> Bool -> Core ()
  Visibility: export
addHintFor : Ref Ctxt Defs => FC -> Name -> Name -> Bool -> Bool -> Core ()
  Visibility: export
addGlobalHint : Ref Ctxt Defs => Name -> Bool -> Core ()
  Visibility: export
addLocalHint : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
addOpenHint : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
dropOpenHint : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setOpenHints : Ref Ctxt Defs => NameMap () -> Core ()
  Visibility: export
addTransform : Ref Ctxt Defs => FC -> Transform -> Core ()
  Visibility: export
clearSavedHints : Ref Ctxt Defs => Core ()
  Visibility: export
setNS : Ref Ctxt Defs => Namespace -> Core ()
  Visibility: export
setNestedNS : Ref Ctxt Defs => List Namespace -> Core ()
  Visibility: export
getNS : Ref Ctxt Defs => Core Namespace
  Visibility: export
getNestedNS : Ref Ctxt Defs => Core (List Namespace)
  Visibility: export
addImported : Ref Ctxt Defs => (ModuleIdent, (Bool, Namespace)) -> Core ()
  Visibility: export
getImported : Ref Ctxt Defs => Core (List (ModuleIdent, (Bool, Namespace)))
  Visibility: export
addDirective : Ref Ctxt Defs => String -> String -> Core ()
  Visibility: export
getDirectives : Ref Ctxt Defs => CG -> Core (List String)
  Visibility: export
extendNS : Ref Ctxt Defs => Namespace -> Core ()
  Visibility: export
withExtendedNS : Ref Ctxt Defs => Namespace -> Core a -> Core a
  Visibility: export
inCurrentNS : Ref Ctxt Defs => Name -> Core Name
  Visibility: export
setVisible : Ref Ctxt Defs => Namespace -> Core ()
  Visibility: export
getVisible : Ref Ctxt Defs => Core (List Namespace)
  Visibility: export
setAllPublic : Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
isAllPublic : Ref Ctxt Defs => Core Bool
  Visibility: export
isVisible : Ref Ctxt Defs => Namespace -> Core Bool
  Visibility: export
getNextEntry : Ref Ctxt Defs => Core Int
  Visibility: export
setNextEntry : Ref Ctxt Defs => Int -> Core ()
  Visibility: export
resetFirstEntry : Ref Ctxt Defs => Core ()
  Visibility: export
getFullName : Ref Ctxt Defs => Name -> Core Name
  Visibility: export
getPPrint : Ref Ctxt Defs => Core PPrinter
  Visibility: export
setPPrint : Ref Ctxt Defs => PPrinter -> Core ()
  Visibility: export
updatePPrint : Ref Ctxt Defs => (PPrinter -> PPrinter) -> Core ()
  Visibility: export
setCG : Ref Ctxt Defs => CG -> Core ()
  Visibility: export
getDirs : Ref Ctxt Defs => Core Dirs
  Visibility: export
addExtraDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
addPackageDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
addPackageSearchPath : Ref Ctxt Defs => String -> Core ()
  Visibility: export
addDataDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
addLibDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
setBuildDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
setDependsDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
setOutputDir : Ref Ctxt Defs => Maybe String -> Core ()
  Visibility: export
setSourceDir : Ref Ctxt Defs => Maybe String -> Core ()
  Visibility: export
setWorkingDir : Ref Ctxt Defs => String -> Core ()
  Visibility: export
getWorkingDir : Core String
  Visibility: export
setExtraDirs : Ref Ctxt Defs => List String -> Core ()
  Visibility: export
setPackageDirs : Ref Ctxt Defs => List String -> Core ()
  Visibility: export
withCtxt : Ref Ctxt Defs => Core a -> Core a
  Visibility: export
setPrefix : Ref Ctxt Defs => String -> Core ()
  Visibility: export
setExtension : Ref Ctxt Defs => LangExt -> Core ()
  Visibility: export
isExtension : LangExt -> Defs -> Bool
  Visibility: export
checkUnambig : Ref Ctxt Defs => FC -> Name -> Core Name
  Visibility: export
lazyActive : Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
setUnboundImplicits : Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
setPrefixRecordProjections : Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
setDefaultTotalityOption : Ref Ctxt Defs => TotalReq -> Core ()
  Visibility: export
setAmbigLimit : Ref Ctxt Defs => Nat -> Core ()
  Visibility: export
setTotalLimit : Ref Ctxt Defs => Nat -> Core ()
  Visibility: export
setAutoImplicitLimit : Ref Ctxt Defs => Nat -> Core ()
  Visibility: export
setNFThreshold : Ref Ctxt Defs => Nat -> Core ()
  Visibility: export
setSearchTimeout : Ref Ctxt Defs => Integer -> Core ()
  Visibility: export
isLazyActive : Ref Ctxt Defs => Core Bool
  Visibility: export
isUnboundImplicits : Ref Ctxt Defs => Core Bool
  Visibility: export
isPrefixRecordProjections : Ref Ctxt Defs => Core Bool
  Visibility: export
getDefaultTotalityOption : Ref Ctxt Defs => Core TotalReq
  Visibility: export
getAmbigLimit : Ref Ctxt Defs => Core Nat
  Visibility: export
getAutoImplicitLimit : Ref Ctxt Defs => Core Nat
  Visibility: export
addForeignImpl : Ref Ctxt Defs => FC -> Name -> String -> Core ()
  Visibility: export
setPair : Ref Ctxt Defs => FC -> Name -> Name -> Name -> Core ()
  Visibility: export
setRewrite : Ref Ctxt Defs => FC -> Name -> Name -> Core ()
  Visibility: export
setFromInteger : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromString : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromChar : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromDouble : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromTTImp : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromName : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
setFromDecls : Ref Ctxt Defs => Name -> Core ()
  Visibility: export
addNameDirective : Ref Ctxt Defs => FC -> Name -> List String -> Core ()
  Visibility: export
isPairType : Ref Ctxt Defs => Name -> Core Bool
  Visibility: export
fstName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
sndName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
getRewrite : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
isEqualTy : Ref Ctxt Defs => Name -> Core Bool
  Visibility: export
fromIntegerName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromStringName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromCharName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromDoubleName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromTTImpName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromNameName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
fromDeclsName : Ref Ctxt Defs => Core (Maybe Name)
  Visibility: export
getPrimNames : Ref Ctxt Defs => Core PrimNames
  Visibility: export
getPrimitiveNames : Ref Ctxt Defs => Core (List Name)
  Visibility: export
isPrimName : List Name -> Name -> Bool
  Visibility: export
addLogLevel : Ref Ctxt Defs => Maybe LogLevel -> Core ()
  Visibility: export
setLogLevel : Ref Ctxt Defs => LogLevel -> Core ()
  Visibility: export
stopLogging : Ref Ctxt Defs => Core ()
  Visibility: export
withLogLevel : Ref Ctxt Defs => LogLevel -> Core a -> Core a
  Visibility: export
setLogTimings : Ref Ctxt Defs => Nat -> Core ()
  Visibility: export
setDebugElabCheck : Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
getSession : Ref Ctxt Defs => Core Session
  Visibility: export
setSession : Ref Ctxt Defs => Session -> Core ()
  Visibility: export
updateSession : Ref Ctxt Defs => (Session -> Session) -> Core ()
  Visibility: export
recordWarning : Ref Ctxt Defs => Warning -> Core ()
  Visibility: export
getTime : Core Integer
  Visibility: export
startTimer : Ref Ctxt Defs => Integer -> String -> Core ()
  Initialise the timer, setting the time in milliseconds after which a
  timeout should be thrown.
  Note: It's important to clear the timer when the operation that might
  timeout is complete, otherwise something else might throw a timeout
  error!

  Visibility: export
clearTimer : Ref Ctxt Defs => Core ()
  Clear the timer

  Visibility: export
checkTimer : Ref Ctxt Defs => Core ()
  If the timer was started more than t milliseconds ago, throw an exception

  Visibility: export
addImportedInc : Ref Ctxt Defs => ModuleIdent -> List (CG, (String, List String)) -> Core ()
  Visibility: export
setIncData : Ref Ctxt Defs => CG -> (String, List String) -> Core ()
  Visibility: export
hide : Ref Ctxt Defs => FC -> Name -> Core ()
  Visibility: export
unhide : Ref Ctxt Defs => FC -> Name -> Core ()
  Visibility: export