- instLevelType : Lean.Core.InstantiateLevelCache
- instLevelValue : Lean.Core.InstantiateLevelCache
Cache for the CoreM
monad
Instances For
- env : Lean.Environment
Current environment.
- nextMacroScope : Lean.MacroScope
Next macro scope. We use macro scopes to avoid accidental name capture.
- ngen : Lean.NameGenerator
Name generator for producing unique
FVarId
s,MVarId
s, andLMVarId
s - traceState : Lean.TraceState
Trace messages
- cache : Lean.Core.Cache
Cache for instantiating universe polymorphic declarations.
- messages : Lean.MessageLog
Message log.
- infoState : Lean.Elab.InfoState
Info tree. We have the info tree here because we want to update it while adding attributes.
State for the CoreM monad.
Instances For
- fileName : String
Name of the file being compiled.
- fileMap : Lean.FileMap
Auxiliary datastructure for converting
String.Pos
into Line/Column number. - options : Lean.Options
- currRecDepth : Nat
- maxRecDepth : Nat
- ref : Lean.Syntax
- currNamespace : Lake.Name
- openDecls : List Lean.OpenDecl
- initHeartbeats : Nat
- maxHeartbeats : Nat
- currMacroScope : Lean.MacroScope
Context for the CoreM monad.
Instances For
CoreM is a monad for manipulating the Lean environment.
It is the base monad for MetaM
.
The main features it provides are:
- name generator state
- environment state
- Lean options context
- the current open namespace
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Restore backtrackable parts of the state.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Return true if ex
was generated by throwMaxHeartbeat
.
This function is a bit hackish. The heartbeat exception should probably be an internal exception.
We used a similar hack at Exception.isMaxRecDepth
Instances For
Creates the expression d → b