- options : Lean.Options
- ref : Lean.Syntax
- autoBoundImplicit : Bool
- ngen : Lean.NameGenerator
- mctx : Lean.MetavarContext
- levelNames : List Lean.Name
@[inline]
Equations
- Lean.Elab.Level.instMonadOptionsLevelElabM = { getOptions := do let a ← read pure a.options }
Equations
- Lean.Elab.Level.instMonadRefLevelElabM = { getRef := do let a ← read pure a.ref, withRef := fun {α} ref x => withReader (fun ctx => { options := ctx.options, ref := ref, autoBoundImplicit := ctx.autoBoundImplicit }) x }
Equations
- Lean.Elab.Level.instAddMessageContextLevelElabM = { addMessageContext := fun msg => pure msg }
Equations
- Lean.Elab.Level.instMonadNameGeneratorLevelElabM = { getNGen := do let a ← get pure a.ngen, setNGen := fun ngen => modify fun s => { ngen := ngen, mctx := s.mctx, levelNames := s.levelNames } }
Equations
- Lean.Elab.Level.mkFreshLevelMVar = do let mvarId ← Lean.mkFreshMVarId modify fun s => { ngen := s.ngen, mctx := Lean.MetavarContext.addLevelMVarDecl s.mctx mvarId, levelNames := s.levelNames } pure (Lean.mkLevelMVar mvarId)