Lean.Elab.Term

Lean.Elab.Term.instInhabitedState = { default := { levelNames := default, syntheticMVars := default, mvarErrorInfos := default, messages := default, letRecsToLift := default, infoState := default } }

source

@[inline]

abbrev Lean.Elab.Term.TermElabM (α : Type) :

Type

Equations

Lean.Elab.TermElabM = ReaderT Lean.Elab.Term.Context (StateRefT' IO.RealWorld Lean.Elab.Term.State Lean.MetaM)

source

@[inline]

abbrev Lean.Elab.Term.TermElab :

Type

Equations

Lean.Elab.Term.TermElab = (Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr)

source

instance Lean.Elab.Term.instMonadTermElabM :

Monad Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadTermElabM = let i := inferInstanceAs (Monad Lean.Elab.TermElabM); Monad.mk

source

instance Lean.Elab.Term.instInhabitedTermElabM {α : Type} :

Inhabited (Lean.Elab.TermElabM α)

Equations

Lean.Elab.Term.instInhabitedTermElabM = { default := throw default }

source

structure Lean.Elab.Term.SavedState :

Type

meta : Lean.Meta.SavedState
elab : Lean.Elab.Term.State

source

instance Lean.Elab.Term.instInhabitedSavedState :

Inhabited Lean.Elab.Term.SavedState

Equations

Lean.Elab.Term.instInhabitedSavedState = { default := { meta := default, elab := default } }

source

def Lean.Elab.Term.saveState :

Lean.Elab.TermElabM Lean.Elab.Term.SavedState

Equations

Lean.Elab.Term.saveState = do let a ← liftM Lean.Meta.saveState let a_1 ← get pure { meta := a, elab := a_1 }

source

def Lean.Elab.Term.SavedState.restore (s : Lean.Elab.Term.SavedState) (restoreInfo : optParam Bool false) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.SavedState.restore s restoreInfo = do let traceState ← Lean.getTraceState let a ← get let infoState : Lean.Elab.InfoState := a.infoState liftM (Lean.Meta.SavedState.restore s.meta) set s.elab Lean.setTraceState traceState if restoreInfo = true then pure PUnit.unit else modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := infoState }

source

instance Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM :

Lean.MonadBacktrack Lean.Elab.Term.SavedState Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM = { saveState := Lean.Elab.Term.saveState, restoreState := fun b => Lean.Elab.Term.SavedState.restore b false }

source

@[inline]

abbrev Lean.Elab.Term.TermElabResult (α : Type) :

Type

Equations

Lean.Elab.Term.TermElabResult α = EStateM.Result Lean.Exception Lean.Elab.Term.SavedState α

source

instance Lean.Elab.Term.instInhabitedTermElabResult {α : Type} [inst : Inhabited α] :

Inhabited (Lean.Elab.Term.TermElabResult α)

Equations

Lean.Elab.Term.instInhabitedTermElabResult = { default := EStateM.Result.ok default default }

source

def Lean.Elab.Term.setMessageLog (messages : Lean.MessageLog) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.setMessageLog messages = modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState }

source

def Lean.Elab.Term.resetMessageLog :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.resetMessageLog = Lean.Elab.Term.setMessageLog { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }

source

def Lean.Elab.Term.getMessageLog :

Lean.Elab.TermElabM Lean.MessageLog

Equations

Lean.Elab.Term.getMessageLog = do let a ← get pure a.messages

source

def Lean.Elab.Term.observing {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM (Lean.Elab.Term.TermElabResult α)

Equations

Lean.Elab.Term.observing x = do let s ← Lean.saveState tryCatch (do let e ← x let sNew ← Lean.saveState Lean.Elab.Term.SavedState.restore s true pure (EStateM.Result.ok e sNew)) fun ex => match ex with | ex@h:(Lean.Exception.error x x_1) => do let sNew ← Lean.saveState Lean.Elab.Term.SavedState.restore s true pure (EStateM.Result.error ex sNew) | ex@h:(Lean.Exception.internal id x) => let _do_jp := fun y => throw ex; if (id == Lean.Elab.postponeExceptionId) = true then do let y ← Lean.Elab.Term.SavedState.restore s true _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Term.applyResult {α : Type} (result : Lean.Elab.Term.TermElabResult α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.applyResult result = match result with | EStateM.Result.ok a r => do Lean.Elab.Term.SavedState.restore r true pure a | EStateM.Result.error ex r => do Lean.Elab.Term.SavedState.restore r true throw ex

source

def Lean.Elab.Term.commitIfDidNotPostpone {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.commitIfDidNotPostpone x = do let r ← Lean.Elab.Term.observing x Lean.Elab.Term.applyResult r

source

def Lean.Elab.Term.getLevelNames :

Lean.Elab.TermElabM (List Lean.Name)

Equations

Lean.Elab.Term.getLevelNames = do let a ← get pure a.levelNames

source

def Lean.Elab.Term.getFVarLocalDecl! (fvar : Lean.Expr) :

Lean.Elab.TermElabM Lean.LocalDecl

Equations

Lean.Elab.Term.getFVarLocalDecl! fvar = do let a ← Lean.getLCtx match Lean.LocalContext.find? a (Lean.Expr.fvarId! fvar) with | some d => pure d | none => panicWithPosWithDecl "Lean.Elab.Term" "Lean.Elab.Term.getFVarLocalDecl!" 231 14 "unreachable code has been reached"

source

instance Lean.Elab.Term.instAddErrorMessageContextTermElabM :

Lean.AddErrorMessageContext Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instAddErrorMessageContextTermElabM = { add := fun ref msg => do let ctx ← read let ref : Lean.Syntax := Lean.Elab.getBetterRef ref ctx.macroStack let msg ← Lean.addMessageContext msg let msg ← Lean.Elab.addMacroStack msg ctx.macroStack pure (ref, msg) }

source

instance Lean.Elab.Term.instMonadLogTermElabM :

Lean.Elab.MonadLog Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadLogTermElabM = Lean.Elab.MonadLog.mk Lean.getRef (do let a ← read pure a.fileName) fun msg => do let ctx ← readThe Lean.Core.Context let msg : Lean.Message := { fileName := msg.fileName, pos := msg.pos, endPos := msg.endPos, severity := msg.severity, caption := msg.caption, data := Lean.MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data } modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := Lean.MessageLog.add msg s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState }

source

def Lean.Elab.Term.getCurrMacroScope :

Lean.Elab.TermElabM Lean.MacroScope

Equations

Lean.Elab.Term.getCurrMacroScope = do let a ← read pure a.currMacroScope

source

def Lean.Elab.Term.getMainModule :

Lean.Elab.TermElabM Lean.Name

Equations

Lean.Elab.Term.getMainModule = do let a ← Lean.getEnv pure (Lean.Environment.mainModule a)

source

def Lean.Elab.Term.withFreshMacroScope {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withFreshMacroScope x = do let fresh ← modifyGetThe Lean.Core.State fun st => (st.nextMacroScope, { env := st.env, nextMacroScope := st.nextMacroScope + 1, ngen := st.ngen, traceState := st.traceState }) withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := ctx.macroStack, currMacroScope := fresh, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x

source

instance Lean.Elab.Term.instMonadQuotationTermElabM :

Lean.MonadQuotation Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadQuotationTermElabM = Lean.MonadQuotation.mk Lean.Elab.Term.getCurrMacroScope Lean.Elab.Term.getMainModule fun {α} => Lean.Elab.Term.withFreshMacroScope

source

instance Lean.Elab.Term.instMonadInfoTreeTermElabM :

Lean.Elab.MonadInfoTree Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadInfoTreeTermElabM = { getInfoState := do let a ← get pure a.infoState, modifyInfoState := fun f => modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := f s.infoState } }

source

def Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo x = do let s ← get let sMeta ← getThe Lean.Meta.State tryFinally (Lean.Elab.withSaveInfoContext x) do modify fun a => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := a.infoState } set sMeta

source

unsafe def Lean.Elab.Term.mkTermElabAttributeUnsafe :

IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab)

Equations

Lean.Elab.Term.mkTermElabAttributeUnsafe = Lean.Elab.mkElabAttribute Lean.Elab.Term.TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term"

source

@[implementedBy Lean.Elab.Term.mkTermElabAttributeUnsafe]

constant Lean.Elab.Term.mkTermElabAttribute :

IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab)

source

constant Lean.Elab.Term.termElabAttribute :

Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab

source

inductive Lean.Elab.Term.LVal :

Type

fieldIdx: Lean.Syntax → Nat → Lean.Elab.Term.LVal
fieldName: Lean.Syntax → String → Option Lean.Name → Lean.Syntax → Lean.Elab.Term.LVal
getOp: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.LVal

source

def Lean.Elab.Term.LVal.getRef :

Lean.Elab.Term.LVal → Lean.Syntax

Equations

Lean.Elab.Term.LVal.getRef x = match x with | Lean.Elab.Term.LVal.fieldIdx ref x => ref | Lean.Elab.Term.LVal.fieldName ref x x_1 x_2 => ref | Lean.Elab.Term.LVal.getOp ref x => ref

source

def Lean.Elab.Term.LVal.isFieldName :

Lean.Elab.Term.LVal → Bool

Equations

Lean.Elab.Term.LVal.isFieldName x = match x with | Lean.Elab.Term.LVal.fieldName x x_1 x_2 x_3 => true | x => false

source

instance Lean.Elab.Term.instToStringLVal :

ToString Lean.Elab.Term.LVal

Equations

Lean.Elab.Term.instToStringLVal = { toString := fun x => match x with | Lean.Elab.Term.LVal.fieldIdx x i => toString i | Lean.Elab.Term.LVal.fieldName x n x_1 x_2 => n | Lean.Elab.Term.LVal.getOp x idx => "[" ++ toString idx ++ "]" }

source

def Lean.Elab.Term.getDeclName? :

Lean.Elab.TermElabM (Option Lean.Name)

Equations

Lean.Elab.Term.getDeclName? = do let a ← read pure a.declName?

source

def Lean.Elab.Term.getLetRecsToLift :

Lean.Elab.TermElabM (List Lean.Elab.Term.LetRecToLift)

Equations

Lean.Elab.Term.getLetRecsToLift = do let a ← get pure a.letRecsToLift

source

def Lean.Elab.Term.isExprMVarAssigned (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.isExprMVarAssigned mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.isExprAssigned a mvarId)

source

def Lean.Elab.Term.getMVarDecl (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM Lean.MetavarDecl

Equations

Lean.Elab.Term.getMVarDecl mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.getDecl a mvarId)

source

def Lean.Elab.Term.assignLevelMVar (mvarId : Lean.MVarId) (val : Lean.Level) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.assignLevelMVar mvarId val = modifyThe Lean.Meta.State fun s => { mctx := Lean.MetavarContext.assignLevel s.mctx mvarId val, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed }

source

def Lean.Elab.Term.withDeclName {α : Type} (name : Lean.Name) (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withDeclName name x = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := some name, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x

source

def Lean.Elab.Term.setLevelNames (levelNames : List Lean.Name) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.setLevelNames levelNames = modify fun s => { levelNames := levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState }

source

def Lean.Elab.Term.withLevelNames {α : Type} (levelNames : List Lean.Name) (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withLevelNames levelNames x = do let levelNamesSaved ← Lean.Elab.Term.getLevelNames Lean.Elab.Term.setLevelNames levelNames tryFinally x (Lean.Elab.Term.setLevelNames levelNamesSaved)

source

def Lean.Elab.Term.withoutErrToSorry {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutErrToSorry x = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := false, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x

source

def Lean.Elab.Term.throwErrorIfErrors :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.throwErrorIfErrors = do let a ← get if Lean.MessageLog.hasErrors a.messages = true then Lean.throwError (Lean.toMessageData "Error(s)") else pure PUnit.unit

source

def Lean.Elab.Term.traceAtCmdPos (cls : Lean.Name) (msg : Unit → Lean.MessageData) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.traceAtCmdPos cls msg = Lean.withRef Lean.Syntax.missing (Lean.Elab.trace cls msg)

source

def Lean.Elab.Term.ppGoal (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM Lean.Format

Equations

Lean.Elab.Term.ppGoal mvarId = liftM (Lean.Meta.ppGoal mvarId)

source

def Lean.Elab.Term.liftLevelM {α : Type} (x : Lean.Elab.Level.LevelElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.liftLevelM x = do let ctx ← read let mctx ← Lean.getMCtx let ngen ← Lean.getNGen let a ← Lean.getOptions let a_1 ← Lean.getRef let lvlCtx : Lean.Elab.Level.Context := { options := a, ref := a_1, autoBoundImplicit := ctx.autoBoundImplicit } let a ← Lean.Elab.Term.getLevelNames match EStateM.run (x lvlCtx) { ngen := ngen, mctx := mctx, levelNames := a } with | EStateM.Result.ok a newS => do liftM (Lean.Meta.setMCtx newS.mctx) Lean.setNGen newS.ngen Lean.Elab.Term.setLevelNames newS.levelNames pure a | EStateM.Result.error ex x => throw ex

source

def Lean.Elab.Term.elabLevel (stx : Lean.Syntax) :

Lean.Elab.TermElabM Lean.Level

Equations

Lean.Elab.Term.elabLevel stx = Lean.Elab.Term.liftLevelM (Lean.Elab.Level.elabLevel stx)

source

def Lean.Elab.Term.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withMacroExpansion beforeStx afterStx x = Lean.Elab.withMacroExpansionInfo beforeStx afterStx (withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x)

source

def Lean.Elab.Term.registerSyntheticMVar (stx : Lean.Syntax) (mvarId : Lean.MVarId) (kind : Lean.Elab.Term.SyntheticMVarKind) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerSyntheticMVar stx mvarId kind = modify fun s => { levelNames := s.levelNames, syntheticMVars := { mvarId := mvarId, stx := stx, kind := kind } :: s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState }

source

def Lean.Elab.Term.registerSyntheticMVarWithCurrRef (mvarId : Lean.MVarId) (kind : Lean.Elab.Term.SyntheticMVarKind) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerSyntheticMVarWithCurrRef mvarId kind = do let a ← Lean.getRef Lean.Elab.Term.registerSyntheticMVar a mvarId kind

source

def Lean.Elab.Term.registerMVarErrorInfo (mvarErrorInfo : Lean.Elab.Term.MVarErrorInfo) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerMVarErrorInfo mvarErrorInfo = modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := Std.RBMap.insert s.mvarErrorInfos mvarErrorInfo.mvarId mvarErrorInfo, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState }

source

def Lean.Elab.Term.registerMVarErrorHoleInfo (mvarId : Lean.MVarId) (ref : Lean.Syntax) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerMVarErrorHoleInfo mvarId ref = Lean.Elab.Term.registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := Lean.Elab.Term.MVarErrorKind.hole, argName? := none }

source

def Lean.Elab.Term.registerMVarErrorImplicitArgInfo (mvarId : Lean.MVarId) (ref : Lean.Syntax) (app : Lean.Expr) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerMVarErrorImplicitArgInfo mvarId ref app = Lean.Elab.Term.registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := Lean.Elab.Term.MVarErrorKind.implicitArg app, argName? := none }

source

def Lean.Elab.Term.registerMVarErrorCustomInfo (mvarId : Lean.MVarId) (ref : Lean.Syntax) (msgData : Lean.MessageData) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerMVarErrorCustomInfo mvarId ref msgData = Lean.Elab.Term.registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := Lean.Elab.Term.MVarErrorKind.custom msgData, argName? := none }

source

def Lean.Elab.Term.getMVarErrorInfo? (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM (Option Lean.Elab.Term.MVarErrorInfo)

Equations

Lean.Elab.Term.getMVarErrorInfo? mvarId = do let a ← get pure (Std.RBMap.find? a.mvarErrorInfos mvarId)

source

def Lean.Elab.Term.registerCustomErrorIfMVar (e : Lean.Expr) (ref : Lean.Syntax) (msgData : Lean.MessageData) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.registerCustomErrorIfMVar e ref msgData = match Lean.Expr.getAppFn e with | Lean.Expr.mvar mvarId x => Lean.Elab.Term.registerMVarErrorCustomInfo mvarId ref msgData | x => pure ()

source

def Lean.Elab.Term.throwMVarError {α : Type} (m : Lean.MessageData) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.throwMVarError m = do let a ← get if Lean.MessageLog.hasErrors a.messages = true then Lean.Elab.throwAbortTerm else Lean.throwError m

source

def Lean.Elab.Term.MVarErrorInfo.logError (mvarErrorInfo : Lean.Elab.Term.MVarErrorInfo) (extraMsg? : Option Lean.MessageData) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.MVarErrorInfo.logError mvarErrorInfo extraMsg? = (fun addArgName appendExtra => match mvarErrorInfo.kind with | Lean.Elab.Term.MVarErrorKind.implicitArg app => do let app ← liftM (Lean.Meta.instantiateMVars app) let msg : Lean.MessageData := addArgName (Function.comp Lean.MessageData.ofFormat Lean.format "don't know how to synthesize implicit argument") let msg : Lean.MessageData := msg ++ (Lean.toMessageData "" ++ Lean.toMessageData (Lean.indentExpr (Lean.Expr.setAppPPExplicitForExposingMVars app)) ++ Lean.toMessageData "") ++ Lean.MessageData.ofFormat Lean.Format.line ++ Function.comp Lean.MessageData.ofFormat Lean.format "context:" ++ Lean.MessageData.ofFormat Lean.Format.line ++ Lean.MessageData.ofGoal mvarErrorInfo.mvarId Lean.Elab.logErrorAt mvarErrorInfo.ref (appendExtra msg) | Lean.Elab.Term.MVarErrorKind.hole => let msg := addArgName (Function.comp Lean.MessageData.ofFormat Lean.format "don't know how to synthesize placeholder") " for argument"; let msg := msg ++ Lean.MessageData.ofFormat Lean.Format.line ++ Function.comp Lean.MessageData.ofFormat Lean.format "context:" ++ Lean.MessageData.ofFormat Lean.Format.line ++ Lean.MessageData.ofGoal mvarErrorInfo.mvarId; Lean.Elab.logErrorAt mvarErrorInfo.ref (Lean.MessageData.tagged `Elab.synthPlaceholder (appendExtra msg)) | Lean.Elab.Term.MVarErrorKind.custom msg => Lean.Elab.logErrorAt mvarErrorInfo.ref (appendExtra msg)) (Lean.Elab.Term.MVarErrorInfo.logError.addArgName mvarErrorInfo) (Lean.Elab.Term.MVarErrorInfo.logError.appendExtra extraMsg?)

source

def Lean.Elab.Term.MVarErrorInfo.logError.addArgName (mvarErrorInfo : Lean.Elab.Term.MVarErrorInfo) (msg : Lean.MessageData) (extra : optParam String "") :

Lean.MessageData

Equations

Lean.Elab.Term.MVarErrorInfo.logError.addArgName mvarErrorInfo msg extra = match mvarErrorInfo.argName? with | none => msg | some argName => if Lean.Name.hasMacroScopes argName = true then msg else msg ++ Function.comp Lean.MessageData.ofFormat Lean.format extra ++ (Lean.toMessageData " '" ++ Lean.toMessageData argName ++ Lean.toMessageData "'")

source

def Lean.Elab.Term.MVarErrorInfo.logError.appendExtra (extraMsg? : Option Lean.MessageData) (msg : Lean.MessageData) :

Lean.MessageData

Equations

Lean.Elab.Term.MVarErrorInfo.logError.appendExtra extraMsg? msg = match extraMsg? with | none => msg | some extraMsg => msg ++ extraMsg

source

def Lean.Elab.Term.logUnassignedUsingErrorInfos (pendingMVarIds : Array Lean.MVarId) (extraMsg? : optParam (Option Lean.MessageData) none) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.logUnassignedUsingErrorInfos pendingMVarIds extraMsg? = do let s ← get let hasOtherErrors : Bool := Lean.MessageLog.hasErrors s.messages let hasNewErrors : Bool := false let alreadyVisited : Lean.MVarIdSet := ∅ let errors : Array Lean.Elab.Term.MVarErrorInfo := #[] let r ← let col := s.mvarErrorInfos; forIn col { fst := hasNewErrors, snd := { fst := errors, snd := alreadyVisited } } fun x r => match x with | (x, mvarErrorInfo) => let hasNewErrors := r.fst; let x := r.snd; let errors := x.fst; let alreadyVisited := x.snd; let mvarId := mvarErrorInfo.mvarId; if Std.RBTree.contains alreadyVisited mvarId = true then do pure PUnit.unit pure (ForInStep.yield { fst := hasNewErrors, snd := { fst := errors, snd := alreadyVisited } }) else let alreadyVisited := Std.RBTree.insert alreadyVisited mvarId; do let mvarDeps ← liftM (Lean.Meta.getMVars (Lean.mkMVar mvarId)) if Array.any mvarDeps (Array.contains pendingMVarIds) 0 (Array.size mvarDeps) = true then let _do_jp := fun hasNewErrors errors y => let hasNewErrors := true; do pure PUnit.unit pure (ForInStep.yield { fst := hasNewErrors, snd := { fst := errors, snd := alreadyVisited } }); if hasOtherErrors = true then do let y ← pure PUnit.unit _do_jp hasNewErrors errors y else let errors := Array.push errors mvarErrorInfo; do let y ← pure PUnit.unit _do_jp hasNewErrors errors y else do pure PUnit.unit pure (ForInStep.yield { fst := hasNewErrors, snd := { fst := errors, snd := alreadyVisited } }) let x : MProd Bool (MProd (Array Lean.Elab.Term.MVarErrorInfo) Lean.MVarIdSet) := r match x with | { fst := hasNewErrors, snd := { fst := errors, snd := alreadyVisited } } => do let r ← forIn errors PUnit.unit fun error r => do Lean.Meta.withMVarContext error.mvarId (Lean.Elab.Term.MVarErrorInfo.logError error extraMsg?) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure hasNewErrors

source

def Lean.Elab.Term.ensureNoUnassignedMVars (decl : Lean.Declaration) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.ensureNoUnassignedMVars decl = do let pendingMVarIds ← liftM (Lean.Meta.getMVarsAtDecl decl) let a ← Lean.Elab.Term.logUnassignedUsingErrorInfos pendingMVarIds none if a = true then Lean.Elab.throwAbortCommand else pure PUnit.unit

source

def Lean.Elab.Term.withoutPostponing {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutPostponing x = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := false, errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x

source

def Lean.Elab.Term.mkExplicitBinder (ident : Lean.Syntax) (type : Lean.Syntax) :

Lean.Syntax

Equations

Lean.Elab.Term.mkExplicitBinder ident type = Lean.mkNode `Lean.Parser.Term.explicitBinder #[Lean.mkAtom "(", Lean.mkNullNode #[ident], Lean.mkNullNode #[Lean.mkAtom ":", type], Lean.mkNullNode, Lean.mkAtom ")"]

source

def Lean.Elab.Term.levelMVarToParam (e : Lean.Expr) (nextParamIdx : optParam Nat 1) :

Lean.Elab.TermElabM (Lean.Expr × Nat)

Equations

Lean.Elab.Term.levelMVarToParam e nextParamIdx = do let mctx ← Lean.getMCtx let levelNames ← Lean.Elab.Term.getLevelNames let r : Lean.MetavarContext.UnivMVarParamResult := Lean.MetavarContext.levelMVarToParam mctx (fun n => List.elem n levelNames) e `u nextParamIdx liftM (Lean.Meta.setMCtx r.mctx) pure (r.expr, r.nextParamIdx)

source

def Lean.Elab.Term.levelMVarToParam' (e : Lean.Expr) :

StateRefT' IO.RealWorld Nat Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.levelMVarToParam' e = do let nextParamIdx ← get let discr ← liftM (Lean.Elab.Term.levelMVarToParam e nextParamIdx) let x : Lean.Expr × Nat := discr match x with | (e, nextParamIdx) => do set nextParamIdx pure e

source

def Lean.Elab.Term.mkFreshBinderName {m : Type → Type} [inst : Monad m] [inst : Lean.MonadQuotation m] :

m Lean.Name

Equations

Lean.Elab.Term.mkFreshBinderName = Lean.withFreshMacroScope (Lean.MonadQuotation.addMacroScope `x)

source

def Lean.Elab.Term.mkFreshIdent {m : Type → Type} [inst : Monad m] [inst : Lean.MonadQuotation m] (ref : Lean.Syntax) :

m Lean.Syntax

Equations

Lean.Elab.Term.mkFreshIdent ref = do let a ← Lean.Elab.Term.mkFreshBinderName pure (Lean.mkIdentFrom ref a)

source

def Lean.Elab.Term.applyAttributesAt (declName : Lean.Name) (attrs : Array Lean.Elab.Attribute) (applicationTime : Lean.AttributeApplicationTime) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.applyAttributesAt declName attrs applicationTime = Lean.Elab.Term.applyAttributesCore declName attrs (some applicationTime)

source

def Lean.Elab.Term.applyAttributes (declName : Lean.Name) (attrs : Array Lean.Elab.Attribute) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.applyAttributes declName attrs = Lean.Elab.Term.applyAttributesCore declName attrs none

source

def Lean.Elab.Term.mkTypeMismatchError (header? : Option String) (e : Lean.Expr) (eType : Lean.Expr) (expectedType : Lean.Expr) :

Lean.Elab.TermElabM Lean.MessageData

Equations

Lean.Elab.Term.mkTypeMismatchError header? e eType expectedType = let header := match header? with | some header => Lean.toMessageData "" ++ Lean.toMessageData header ++ Lean.toMessageData " " | none => Lean.toMessageData "type mismatch" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "\n"; do let a ← liftM (Lean.Meta.mkHasTypeButIsExpectedMsg eType expectedType) pure (Lean.toMessageData "" ++ Lean.toMessageData header ++ Lean.toMessageData "" ++ Lean.toMessageData a ++ Lean.toMessageData "")

source

def Lean.Elab.Term.throwTypeMismatchError {α : Type} (header? : Option String) (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (extraMsg? : optParam (Option Lean.MessageData) none) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.throwTypeMismatchError header? expectedType eType e f? extraMsg? = let extraMsg := Lean.Format.nil; match f? with | none => do let a ← Lean.Elab.Term.mkTypeMismatchError header? e eType expectedType Lean.throwError (Lean.toMessageData "" ++ Lean.toMessageData a ++ Lean.toMessageData "" ++ Lean.toMessageData extraMsg ++ Lean.toMessageData "") | some f => liftM (Lean.Meta.throwAppTypeMismatch f e (Lean.MessageData.ofFormat extraMsg))

source

def Lean.Elab.Term.withoutMacroStackAtErr {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutMacroStackAtErr x = withTheReader Lean.Core.Context (fun ctx => { options := Lean.Option.set ctx.options Lean.Elab.pp.macroStack false, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x

source

@[inline]

abbrev Lean.Elab.Term.ContainsPendingMVar.M (α : Type) :

Type

Equations

Lean.Elab.Term.ContainsPendingMVar.M = Lean.MonadCacheT Lean.Expr Unit (OptionT Lean.Elab.TermElabM)

source

partial def Lean.Elab.Term.ContainsPendingMVar.visit (e : Lean.Expr) :

Lean.Elab.Term.ContainsPendingMVar.M Unit

source

def Lean.Elab.Term.containsPendingMVar (e : Lean.Expr) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.containsPendingMVar e = do let a ← OptionT.run (Lean.MonadCacheT.run (Lean.Elab.Term.ContainsPendingMVar.visit e)) match a with | some x => pure false | none => pure true

source

def Lean.Elab.Term.synthesizeInstMVarCore (instMVar : Lean.MVarId) (maxResultSize? : optParam (Option Nat) none) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.synthesizeInstMVarCore instMVar maxResultSize? = do let instMVarDecl ← Lean.Elab.Term.getMVarDecl instMVar let type : Lean.Expr := instMVarDecl.type let type ← liftM (Lean.Meta.instantiateMVars type) let result ← liftM (Lean.Meta.trySynthInstance type maxResultSize?) match result with | Lean.LOption.some val => do let a ← Lean.Elab.Term.isExprMVarAssigned instMVar let _do_jp : PUnit → Lean.Elab.TermElabM Bool := fun y => pure true if a = true then do let oldVal ← liftM (Lean.Meta.instantiateMVars (Lean.mkMVar instMVar)) let a ← liftM (Lean.Meta.isDefEq oldVal val) if a = true then do let y ← pure PUnit.unit _do_jp y else do let a ← Lean.Elab.Term.containsPendingMVar oldVal <||> Lean.Elab.Term.containsPendingMVar val let _do_jp : PUnit → Lean.Elab.TermElabM Bool := fun y => do let oldValType ← liftM (Lean.Meta.inferType oldVal) let valType ← liftM (Lean.Meta.inferType val) let a ← liftM (Lean.Meta.isDefEq oldValType valType) let _do_jp : PUnit → Lean.Elab.TermElabM Bool := fun y => do let y ← Lean.throwError (Lean.toMessageData "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized" ++ Lean.toMessageData (Lean.indentExpr val) ++ Lean.toMessageData "\ninferred" ++ Lean.toMessageData (Lean.indentExpr oldVal) ++ Lean.toMessageData "") _do_jp y if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "synthesized type class instance type is not definitionally equal to expected type, synthesized" ++ Lean.toMessageData (Lean.indentExpr val) ++ Lean.toMessageData "\nhas type" ++ Lean.toMessageData (Lean.indentExpr valType) ++ Lean.toMessageData "\nexpected" ++ Lean.toMessageData (Lean.indentExpr oldValType) ++ Lean.toMessageData "") _do_jp y if a = true then pure false else do let y ← pure PUnit.unit _do_jp y else do let a ← liftM (Lean.Meta.isDefEq (Lean.mkMVar instMVar) val) if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "failed to assign synthesized type class instance" ++ Lean.toMessageData (Lean.indentExpr val) ++ Lean.toMessageData "") _do_jp y | Lean.LOption.undef => pure false | Lean.LOption.none => do let a ← read if a.ignoreTCFailures = true then pure false else Lean.throwError (Lean.toMessageData "failed to synthesize instance" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "")

source

constant Lean.Elab.Term.autoLift :

Lean.Option Bool

source

constant Lean.Elab.Term.maxCoeSize :

Lean.Option Nat

source

def Lean.Elab.Term.synthesizeCoeInstMVarCore (instMVar : Lean.MVarId) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.synthesizeCoeInstMVarCore instMVar = do let a ← Lean.getOptions Lean.Elab.Term.synthesizeInstMVarCore instMVar (some (Lean.Option.get a Lean.Elab.Term.maxCoeSize))

source

def Lean.Elab.Term.tryCoeThunk? (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.tryCoeThunk? expectedType eType e = match expectedType with | Lean.Expr.app (Lean.Expr.const (Lean.Name.str Lean.Name.anonymous "Thunk" x_2) u x) arg x_1 => do let a ← liftM (Lean.Meta.isDefEq eType arg) if a = true then pure (some (Lean.mkApp2 (Lean.mkConst `Thunk.mk u) arg (Lean.mkSimpleThunk e))) else pure none | x => pure none

source

def Lean.Elab.Term.mkCoe (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (errorMsgHeader? : optParam (Option String) none) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.mkCoe expectedType eType e f? errorMsgHeader? = do let u ← liftM (Lean.Meta.getLevel eType) let v ← liftM (Lean.Meta.getLevel expectedType) let coeTInstType : Lean.Expr := Lean.mkAppN (Lean.mkConst `CoeT [u, v]) #[eType, e, expectedType] let mvar ← liftM (Lean.Meta.mkFreshExprMVar (some coeTInstType) Lean.MetavarKind.synthetic Lean.Name.anonymous) let eNew : Lean.Expr := Lean.mkAppN (Lean.mkConst `CoeT.coe [u, v]) #[eType, e, expectedType, mvar] let mvarId : Lean.MVarId := Lean.Expr.mvarId! mvar tryCatch (Lean.Elab.Term.withoutMacroStackAtErr do let a ← Lean.Elab.Term.synthesizeCoeInstMVarCore mvarId if a = true then liftM (Lean.Meta.expandCoe eNew) else do let mvarAux ← liftM (Lean.Meta.mkFreshExprMVar (some expectedType) Lean.MetavarKind.syntheticOpaque Lean.Name.anonymous) Lean.Elab.Term.registerSyntheticMVarWithCurrRef (Lean.Expr.mvarId! mvarAux) (Lean.Elab.Term.SyntheticMVarKind.coe errorMsgHeader? eNew expectedType eType e f?) pure mvarAux) fun ex => match ex with | Lean.Exception.error x msg => Lean.Elab.Term.throwTypeMismatchError errorMsgHeader? expectedType eType e f? (some msg) | x => Lean.Elab.Term.throwTypeMismatchError errorMsgHeader? expectedType eType e f? none

source

def Lean.Elab.Term.isTypeApp? (type : Lean.Expr) :

Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Equations

Lean.Elab.Term.isTypeApp? type = do let type ← Lean.Meta.withReducible (liftM (Lean.Meta.whnf type)) match type with | Lean.Expr.app m α x => do let a ← liftM (Lean.Meta.instantiateMVars m) let a_1 ← liftM (Lean.Meta.instantiateMVars α) pure (some (a, a_1)) | x => pure none

source

def Lean.Elab.Term.synthesizeInst (type : Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.synthesizeInst type = do let type ← liftM (Lean.Meta.instantiateMVars type) let a ← liftM (Lean.Meta.trySynthInstance type none) match a with | Lean.LOption.some val => pure val | Lean.LOption.undef => Lean.throwError (Lean.toMessageData "failed to synthesize instance" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") | Lean.LOption.none => Lean.throwError (Lean.toMessageData "failed to synthesize instance" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "")

source

def Lean.Elab.Term.isMonadApp (type : Lean.Expr) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.isMonadApp type = do let discr ← Lean.Elab.Term.isTypeApp? type match discr with | some (m, x) => do let a ← liftM (Lean.Meta.isMonad? m) pure (Option.isSome a) | x => pure false

source

def Lean.Elab.Term.ensureHasTypeAux (expectedType? : Option Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (errorMsgHeader? : optParam (Option String) none) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.ensureHasTypeAux expectedType? eType e f? errorMsgHeader? = match expectedType? with | none => pure e | some expectedType => do let a ← liftM (Lean.Meta.isDefEq eType expectedType) if a = true then pure e else Lean.Elab.Term.tryLiftAndCoe errorMsgHeader? expectedType eType e f?

source

def Lean.Elab.Term.ensureHasType (expectedType? : Option Lean.Expr) (e : Lean.Expr) (errorMsgHeader? : optParam (Option String) none) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.ensureHasType expectedType? e errorMsgHeader? = match expectedType? with | none => pure e | x => do let eType ← liftM (Lean.Meta.inferType e) Lean.Elab.Term.ensureHasTypeAux expectedType? eType e none errorMsgHeader?

source

def Lean.Elab.Term.tryPostpone :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.tryPostpone = do let a ← read if a.mayPostpone = true then Lean.Elab.throwPostpone else pure PUnit.unit

source

def Lean.Elab.Term.tryPostponeIfMVar (e : Lean.Expr) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.tryPostponeIfMVar e = do let e ← liftM (Lean.Meta.whnfR e) if Lean.Expr.isMVar (Lean.Expr.getAppFn e) = true then Lean.Elab.Term.tryPostpone else pure PUnit.unit

source

def Lean.Elab.Term.tryPostponeIfNoneOrMVar (e? : Option Lean.Expr) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.tryPostponeIfNoneOrMVar e? = match e? with | some e => Lean.Elab.Term.tryPostponeIfMVar e | none => Lean.Elab.Term.tryPostpone

source

def Lean.Elab.Term.tryPostponeIfHasMVars (expectedType? : Option Lean.Expr) (msg : String) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.tryPostponeIfHasMVars expectedType? msg = do Lean.Elab.Term.tryPostponeIfNoneOrMVar expectedType? let discr ← pure expectedType? match discr with | some expectedType => do let expectedType ← liftM (Lean.Meta.instantiateMVars expectedType) let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Expr := fun y => pure expectedType if Lean.Expr.hasExprMVar expectedType = true then do Lean.Elab.Term.tryPostpone let y ← Lean.throwError (Lean.toMessageData "" ++ Lean.toMessageData msg ++ Lean.toMessageData ", expected type contains metavariables" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => Lean.throwError (Lean.toMessageData "" ++ Lean.toMessageData msg ++ Lean.toMessageData ", expected type must be known")

source

def Lean.Elab.Term.saveContext :

Lean.Elab.TermElabM Lean.Elab.Term.SavedContext

Equations

Lean.Elab.Term.saveContext = do let a ← read let a_1 ← read let a_2 ← Lean.getOptions let a_3 ← Lean.getOpenDecls let a_4 ← read pure { declName? := a_1.declName?, options := a_2, openDecls := a_3, macroStack := a.macroStack, errToSorry := a_4.errToSorry }

source

def Lean.Elab.Term.withSavedContext {α : Type} (savedCtx : Lean.Elab.Term.SavedContext) (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withSavedContext savedCtx x = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := savedCtx.declName?, macroStack := savedCtx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := savedCtx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) (withTheReader Lean.Core.Context (fun ctx => { options := savedCtx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := savedCtx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x)

source

def Lean.Elab.Term.getSyntheticMVarDecl? (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM (Option Lean.Elab.Term.SyntheticMVarDecl)

Equations

Lean.Elab.Term.getSyntheticMVarDecl? mvarId = do let a ← get pure (List.find? (fun d => d.mvarId == mvarId) a.syntheticMVars)

source

def Lean.Elab.Term.mkSaveInfoAnnotation (e : Lean.Expr) :

Lean.Expr

Equations

Lean.Elab.Term.mkSaveInfoAnnotation e = if Lean.Expr.isMVar e = true then Lean.mkAnnotation `save_info e else e

source

def Lean.Elab.Term.isSaveInfoAnnotation? (e : Lean.Expr) :

Option Lean.Expr

Equations

Lean.Elab.Term.isSaveInfoAnnotation? e = Lean.annotation? `save_info e

source

partial def Lean.Elab.Term.removeSaveInfoAnnotation (e : Lean.Expr) :

Lean.Expr

source

def Lean.Elab.Term.mkTermInfo (elaborator : Lean.Name) (stx : Lean.Syntax) (e : Lean.Expr) (expectedType? : optParam (Option Lean.Expr) none) (lctx? : optParam (Option Lean.LocalContext) none) (isBinder : optParam Bool false) :

Lean.Elab.TermElabM (Lean.Elab.Info ⊕ Lean.MVarId)

Equations

Lean.Elab.Term.mkTermInfo elaborator stx e expectedType? lctx? isBinder = let isHole? := match e with | Lean.Expr.mvar mvarId x => do let a ← Lean.Elab.Term.getSyntheticMVarDecl? mvarId match a with | some { mvarId := x_2, stx := x_3, kind := Lean.Elab.Term.SyntheticMVarKind.tactic x x_1 } => pure (some mvarId) | some { mvarId := x_1, stx := x_2, kind := Lean.Elab.Term.SyntheticMVarKind.postponed x } => pure (some mvarId) | x => pure none | x => pure none; do let a ← isHole? match a with | some mvarId => pure (Sum.inr mvarId) | none => let e := Lean.Elab.Term.removeSaveInfoAnnotation e; do let a ← Lean.getLCtx pure (Sum.inl (Lean.Elab.Info.ofTermInfo { toElabInfo := { elaborator := elaborator, stx := stx }, lctx := Option.getD lctx? a, expectedType? := expectedType?, expr := e, isBinder := isBinder }))

source

def Lean.Elab.Term.addTermInfo (stx : Lean.Syntax) (e : Lean.Expr) (expectedType? : optParam (Option Lean.Expr) none) (lctx? : optParam (Option Lean.LocalContext) none) (elaborator : optParam Lean.Name Lean.Name.anonymous) (isBinder : optParam Bool false) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.addTermInfo stx e expectedType? lctx? elaborator isBinder = discard (Lean.Elab.withInfoContext' (pure ()) fun x => Lean.Elab.Term.mkTermInfo elaborator stx e expectedType? lctx? isBinder)

source

instance Lean.Elab.Term.instMonadMacroAdapterTermElabM :

Lean.Elab.MonadMacroAdapter Lean.Elab.TermElabM

Equations

Lean.Elab.Term.instMonadMacroAdapterTermElabM = { getCurrMacroScope := Lean.getCurrMacroScope, getNextMacroScope := do let a ← getThe Lean.Core.State pure a.nextMacroScope, setNextMacroScope := fun next => modifyThe Lean.Core.State fun s => { env := s.env, nextMacroScope := next, ngen := s.ngen, traceState := s.traceState } }

source

def Lean.Elab.Term.mkNoImplicitLambdaAnnotation (type : Lean.Expr) :

Lean.Expr

Equations

Lean.Elab.Term.mkNoImplicitLambdaAnnotation type = Lean.mkAnnotation `noImplicitLambda type

source

def Lean.Elab.Term.hasNoImplicitLambdaAnnotation (type : Lean.Expr) :

Bool

Equations

Lean.Elab.Term.hasNoImplicitLambdaAnnotation type = Option.isSome (Lean.annotation? `noImplicitLambda type)

source

def Lean.Elab.Term.blockImplicitLambda (stx : Lean.Syntax) :

Bool

Equations

Lean.Elab.Term.blockImplicitLambda stx = let stx := Lean.Elab.Term.dropTermParens stx; Lean.Elab.Term.isExplicit stx || Lean.Elab.Term.isExplicitApp stx || Lean.Elab.Term.isLambdaWithImplicit stx || Lean.Elab.Term.isHole stx || Lean.Elab.Term.isTacticBlock stx || Lean.Elab.Term.isNoImplicitLambda stx || Lean.Elab.Term.isTypeAscription stx

source

def Lean.Elab.Term.addDotCompletionInfo (stx : Lean.Syntax) (e : Lean.Expr) (expectedType? : Option Lean.Expr) (field? : optParam (Option Lean.Syntax) none) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.addDotCompletionInfo stx e expectedType? field? = do let a ← Lean.getLCtx Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.dot { toElabInfo := { elaborator := Lean.Name.anonymous, stx := stx }, lctx := a, expectedType? := expectedType?, expr := e, isBinder := false } field? expectedType?)

source

def Lean.Elab.Term.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabTerm stx expectedType? catchExPostpone implicitLambda = Lean.withRef stx (Lean.Elab.Term.elabTermAux expectedType? catchExPostpone implicitLambda stx)

source

def Lean.Elab.Term.elabTermEnsuringType (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) (errorMsgHeader? : optParam (Option String) none) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabTermEnsuringType stx expectedType? catchExPostpone implicitLambda errorMsgHeader? = do let e ← Lean.Elab.Term.elabTerm stx expectedType? catchExPostpone implicitLambda Lean.withRef stx (Lean.Elab.Term.ensureHasType expectedType? e errorMsgHeader?)

source

def Lean.Elab.Term.withoutPending {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutPending x = do let saved ← get tryFinally x (modify fun s => { levelNames := saved.levelNames, syntheticMVars := saved.syntheticMVars, mvarErrorInfos := saved.mvarErrorInfos, messages := s.messages, letRecsToLift := saved.letRecsToLift, infoState := s.infoState })

source

def Lean.Elab.Term.commitIfNoErrors? {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM (Option α)

Equations

Lean.Elab.Term.commitIfNoErrors? x = do let saved ← Lean.saveState modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, letRecsToLift := s.letRecsToLift, infoState := s.infoState } let r ← tryCatch (do let a ← x let a_1 ← get if Lean.MessageLog.hasErrors a_1.messages = true then do Lean.restoreState saved pure none else do modify fun s => { levelNames := s.levelNames, syntheticMVars := s.syntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := saved.elab.messages ++ s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState } pure (some a)) fun x => do Lean.restoreState saved pure none pure r

source

def Lean.Elab.Term.adaptExpander (exp : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax) :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.adaptExpander exp stx expectedType? = do let stx' ← exp stx Lean.Elab.Term.withMacroExpansion stx stx' (Lean.Elab.Term.elabTerm stx' expectedType? true true)

source

def Lean.Elab.Term.mkInstMVar (type : Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.mkInstMVar type = do let mvar ← liftM (Lean.Meta.mkFreshExprMVar (some type) Lean.MetavarKind.synthetic Lean.Name.anonymous) let mvarId : Lean.MVarId := Lean.Expr.mvarId! mvar let a ← Lean.Elab.Term.synthesizeInstMVarCore mvarId none let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Expr := fun y => pure mvar if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.Term.registerSyntheticMVarWithCurrRef mvarId Lean.Elab.Term.SyntheticMVarKind.typeClass _do_jp y

source

def Lean.Elab.Term.ensureType (e : Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.ensureType e = do let a ← liftM (Lean.Meta.isType e) if a = true then pure e else do let eType ← liftM (Lean.Meta.inferType e) let u ← liftM Lean.Meta.mkFreshLevelMVar let a ← liftM (Lean.Meta.isDefEq eType (Lean.mkSort u)) if a = true then pure e else Lean.Elab.Term.tryCoeSort eType e

source

def Lean.Elab.Term.elabType (stx : Lean.Syntax) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabType stx = do let u ← liftM Lean.Meta.mkFreshLevelMVar let type ← Lean.Elab.Term.elabTerm stx (some (Lean.mkSort u)) true true Lean.withRef stx (Lean.Elab.Term.ensureType type)

source

def Lean.Elab.Term.withAutoBoundImplicit {α : Type} (k : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withAutoBoundImplicit k = do let a ← Lean.getOptions let flag : Bool := Lean.Option.get a Lean.Elab.autoBoundImplicitLocal if flag = true then withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := flag, autoBoundImplicits := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 }, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) ((fun loop => do let a ← Lean.saveState loop a) (Lean.Elab.Term.withAutoBoundImplicit.loop k)) else k

source

partial def Lean.Elab.Term.withAutoBoundImplicit.loop {α : Type} (k : Lean.Elab.TermElabM α) (s : Lean.Elab.Term.SavedState) :

Lean.Elab.TermElabM α

source

def Lean.Elab.Term.withoutAutoBoundImplicit {α : Type} (k : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutAutoBoundImplicit k = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := false, autoBoundImplicits := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 }, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) k

source

def Lean.Elab.Term.addAutoBoundImplicits (xs : Array Lean.Expr) :

Lean.Elab.TermElabM (Array Lean.Expr)

Equations

Lean.Elab.Term.addAutoBoundImplicits xs = do let a ← read let autoBoundImplicits : Std.PArray Lean.Expr := a.autoBoundImplicits let r ← forIn autoBoundImplicits PUnit.unit fun auto r => do let localDecl ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! auto)) let r ← forIn xs PUnit.unit fun x r => do let a ← Lean.getMCtx if Lean.MetavarContext.localDeclDependsOn a localDecl (Lean.Expr.fvarId! x) = true then do Lean.throwError (Lean.toMessageData "invalid auto implicit argument '" ++ Lean.toMessageData auto ++ Lean.toMessageData "', it depends on explicitly provided argument '" ++ Lean.toMessageData x ++ Lean.toMessageData "'") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure (Std.PersistentArray.toArray autoBoundImplicits ++ xs)

source

def Lean.Elab.Term.mkAuxName (suffix : Lean.Name) :

Lean.Elab.TermElabM Lean.Name

Equations

Lean.Elab.Term.mkAuxName suffix = do let a ← read match a.declName? with | none => Lean.throwError (Lean.toMessageData "auxiliary declaration cannot be created when declaration name is not available") | some declName => Lean.mkAuxName (declName ++ suffix) 1

source

def Lean.Elab.Term.isLetRecAuxMVar (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.isLetRecAuxMVar mvarId = let cls := `Elab.letrec; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Bool := fun y => do let a ← Lean.getMCtx let mvarId : Lean.MVarId := Lean.MetavarContext.getDelayedRoot a mvarId let cls : Lean.Name := `Elab.letrec let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Bool := fun y => do let a ← get pure (List.any a.letRecsToLift fun a => a.mvarId == mvarId) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "mvarId root: " ++ Lean.toMessageData (Lean.mkMVar mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let a ← get let y ← Lean.addTrace cls (Lean.toMessageData "mvarId: " ++ Lean.toMessageData (Lean.mkMVar mvarId) ++ Lean.toMessageData " letrecMVars: " ++ Lean.toMessageData (List.map (fun a => Lean.mkMVar a.mvarId) a.letRecsToLift) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Term.resolveLocalName (n : Lean.Name) :

Lean.Elab.TermElabM (Option (Lean.Expr × List String))

Equations

Lean.Elab.Term.resolveLocalName n = do let lctx ← Lean.getLCtx let view : Lean.MacroScopesView := Lean.extractMacroScopes n (fun loop => pure (loop view.name [])) (Lean.Elab.Term.resolveLocalName.loop lctx view)

source

def Lean.Elab.Term.resolveLocalName.loop (lctx : Lean.LocalContext) (view : Lean.MacroScopesView) (n : Lean.Name) (projs : List String) :

Option (Lean.Expr × List String)

source

def Lean.Elab.Term.isLocalIdent? (stx : Lean.Syntax) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.isLocalIdent? stx = match stx with | Lean.Syntax.ident x x_1 val x_2 => do let r? ← Lean.Elab.Term.resolveLocalName val match r? with | some (fvar, []) => pure (some fvar) | x => pure none | x => pure none

source

def Lean.Elab.Term.mkConst (constName : Lean.Name) (explicitLevels : optParam (List Lean.Level) []) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.mkConst constName explicitLevels = do let cinfo ← Lean.getConstInfo constName if List.length explicitLevels > List.length (Lean.ConstantInfo.levelParams cinfo) then Lean.throwError (Lean.toMessageData "too many explicit universe levels for '" ++ Lean.toMessageData constName ++ Lean.toMessageData "'") else let numMissingLevels := List.length (Lean.ConstantInfo.levelParams cinfo) - List.length explicitLevels; do let us ← liftM (Lean.Meta.mkFreshLevelMVars numMissingLevels) pure (Lean.mkConst constName (explicitLevels ++ us))

source

def Lean.Elab.Term.resolveName (stx : Lean.Syntax) (n : Lean.Name) (preresolved : List (Lean.Name × List String)) (explicitLevels : List Lean.Level) (expectedType? : optParam (Option Lean.Expr) none) :

Lean.Elab.TermElabM (List (Lean.Expr × List String))

Equations

Lean.Elab.Term.resolveName stx n preresolved explicitLevels expectedType? = (fun process => do let r ← tryCatch (do let a ← Lean.Elab.Term.resolveLocalName n let _do_jp : PUnit → Lean.Elab.TermElabM (DoResultPR (List (Lean.Expr × List String)) (List (Lean.Expr × List String)) PUnit) := fun y => do let ctx ← read let _do_jp : PUnit → Lean.Elab.TermElabM (DoResultPR (List (Lean.Expr × List String)) (List (Lean.Expr × List String)) PUnit) := fun y => if List.isEmpty preresolved = true then do let a ← Lean.resolveGlobalName n let y ← process a pure (DoResultPR.pure y PUnit.unit) else do let y ← process preresolved pure (DoResultPR.pure y PUnit.unit) match List.findSome? (fun x => match x with | (n, projs) => Option.map (fun a => (a, projs)) (Lean.NameMap.find? ctx.sectionFVars n)) preresolved with | some (e, projs) => pure (DoResultPR.return [(e, projs)] PUnit.unit) | x => do let y ← pure PUnit.unit _do_jp y match a with | some (e, projs) => let _do_jp := fun y => pure (DoResultPR.return [(e, projs)] PUnit.unit); if List.isEmpty explicitLevels = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid use of explicit universe parameters, '" ++ Lean.toMessageData e ++ Lean.toMessageData "' is a local") _do_jp y | x => do let y ← pure PUnit.unit _do_jp y) fun ex => let _do_jp := fun y => do let y ← throw ex pure (DoResultPR.pure y PUnit.unit); if (List.isEmpty preresolved && List.isEmpty explicitLevels) = true then do let a ← Lean.getLCtx let y ← Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.id stx (Lean.Syntax.getId stx) false a expectedType?) _do_jp y else do let y ← pure PUnit.unit _do_jp y match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b) (Lean.Elab.Term.resolveName.process stx n preresolved explicitLevels expectedType?)

source

def Lean.Elab.Term.resolveName.process (stx : Lean.Syntax) (n : Lean.Name) (preresolved : List (Lean.Name × List String)) (explicitLevels : List Lean.Level) (expectedType? : optParam (Option Lean.Expr) none) (candidates : List (Lean.Name × List String)) :

Lean.Elab.TermElabM (List (Lean.Expr × List String))

Equations

Lean.Elab.Term.resolveName.process stx n preresolved explicitLevels expectedType? candidates = let _do_jp := fun y => let _do_jp := fun y => Lean.Elab.Term.mkConsts candidates explicitLevels; if (List.isEmpty preresolved && List.isEmpty explicitLevels) = true then do let a ← Lean.getLCtx let y ← Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.id stx (Lean.Syntax.getId stx) false a expectedType?) _do_jp y else do let y ← pure PUnit.unit _do_jp y; if List.isEmpty candidates = true then do let a ← read if (a.autoBoundImplicit && Lean.Elab.isValidAutoBoundImplicitName n) = true then do let y ← Lean.Elab.throwAutoBoundImplicitLocal n _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unknown identifier '" ++ Lean.toMessageData (Lean.mkConst n) ++ Lean.toMessageData "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Term.resolveName' (ident : Lean.Syntax) (explicitLevels : List Lean.Level) (expectedType? : optParam (Option Lean.Expr) none) :

Lean.Elab.TermElabM (List (Lean.Expr × Lean.Syntax × List Lean.Syntax))

Equations

Lean.Elab.Term.resolveName' ident explicitLevels expectedType? = match ident with | Lean.Syntax.ident info rawStr n preresolved => do let r ← Lean.Elab.Term.resolveName ident n preresolved explicitLevels expectedType? List.mapM (fun x => match x with | (c, fields) => let ids := Lean.Syntax.identComponents ident (some (List.length fields)); pure (c, List.head! ids, List.tail! ids)) r | x => Lean.throwError (Lean.toMessageData "identifier expected")

source

def Lean.Elab.Term.resolveId? (stx : Lean.Syntax) (kind : optParam String "term") (withInfo : optParam Bool false) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.resolveId? stx kind withInfo = match stx with | Lean.Syntax.ident x x_1 val preresolved => let _do_jp := fun rs => let rs := List.filter (fun x => match x with | (f, projs) => List.isEmpty projs) rs; let fs := List.map (fun x => match x with | (f, x) => f) rs; match fs with | [] => pure none | [f] => let _do_jp := fun y => pure (some f); if withInfo = true then do let y ← Lean.Elab.Term.addTermInfo stx f none none Lean.Name.anonymous false _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => Lean.throwError (Lean.toMessageData "ambiguous " ++ Lean.toMessageData kind ++ Lean.toMessageData ", use fully qualified name, possible interpretations " ++ Lean.toMessageData fs ++ Lean.toMessageData ""); do let y ← tryCatch (Lean.Elab.Term.resolveName stx val preresolved [] none) fun x => pure [] _do_jp y | x => Lean.throwError (Lean.toMessageData "identifier expected")

source

def Lean.Elab.Term.TermElabM.run {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context Lean.Elab.Term.mkSomeContext) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := [], mvarErrorInfos := ∅, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, letRecsToLift := [], infoState := { enabled := false, assignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, trees := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } }) :

Lean.MetaM (α × Lean.Elab.Term.State)

Equations

Lean.Elab.Term.TermElabM.run x ctx s = Lean.Meta.withConfig Lean.Elab.Term.setElabConfig (StateRefT'.run (x ctx) s)

source

@[inline]

def Lean.Elab.Term.TermElabM.run' {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context Lean.Elab.Term.mkSomeContext) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := [], mvarErrorInfos := ∅, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, letRecsToLift := [], infoState := { enabled := false, assignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, trees := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } }) :

Lean.MetaM α

Equations

Lean.Elab.Term.TermElabM.run' x ctx s = (fun a => a.fst) <$> Lean.Elab.Term.TermElabM.run x ctx s

source

def Lean.Elab.Term.TermElabM.toIO {α : Type} (x : Lean.Elab.TermElabM α) (ctxCore : Lean.Core.Context) (sCore : Lean.Core.State) (ctxMeta : Lean.Meta.Context) (sMeta : Lean.Meta.State) (ctx : Lean.Elab.Term.Context) (s : Lean.Elab.Term.State) :

IO (α × Lean.Core.State × Lean.Meta.State × Lean.Elab.Term.State)

Equations

Lean.Elab.Term.TermElabM.toIO x ctxCore sCore ctxMeta sMeta ctx s = do let discr ← Lean.Meta.MetaM.toIO (Lean.Elab.Term.TermElabM.run x ctx s) ctxCore sCore ctxMeta sMeta let x : (α × Lean.Elab.Term.State) × Lean.Core.State × Lean.Meta.State := discr match x with | ((a, s), sCore, sMeta) => pure (a, sCore, sMeta, s)

source

instance Lean.Elab.Term.instMetaEvalTermElabM {α : Type} [inst : Lean.MetaEval α] :

Lean.MetaEval (Lean.Elab.TermElabM α)

Equations

Lean.Elab.Term.instMetaEvalTermElabM = { eval := fun env opts x x_1 => let x := tryFinally x do let s ← get Lean.MessageLog.forM s.messages fun msg => do let a ← liftM (Lean.Message.toString msg false) liftM (IO.println a); Lean.MetaEval.eval env opts (Lean.Elab.Term.TermElabM.run' x Lean.Elab.Term.mkSomeContext { levelNames := [], syntheticMVars := [], mvarErrorInfos := ∅, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, letRecsToLift := [], infoState := { enabled := false, assignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, trees := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } }) true }

source

unsafe def Lean.Elab.Term.evalExpr (α : Type) (typeName : Lean.Name) (value : Lean.Expr) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.evalExpr α typeName value = Lean.withoutModifyingEnv do let name ← liftM (Lean.mkFreshUserName `_tmp) let type ← liftM (Lean.Meta.inferType value) let type ← liftM (Lean.Meta.whnfD type) let _do_jp : PUnit → Lean.Elab.TermElabM α := fun y => let decl := Lean.Declaration.defnDecl { toConstantVal := { name := name, levelParams := [], type := type }, value := value, hints := Lean.ReducibilityHints.opaque, safety := Lean.DefinitionSafety.unsafe }; do Lean.Elab.Term.ensureNoUnassignedMVars decl Lean.addAndCompile decl Lean.evalConst α name if Lean.Expr.isConstOf type typeName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unexpected type at evalExpr" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y

source

def Lean.Elab.Term.withoutPostponingUniverseConstraints {α : Type} (x : Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withoutPostponingUniverseConstraints x = do let postponed ← liftM Lean.Meta.getResetPostponed let r ← tryCatch (do let a ← x let a_1 ← liftM (Lean.Meta.processPostponed false true) let _do_jp : PUnit → Lean.Elab.TermElabM (DoResultPR α α PUnit) := fun y => do liftM (Lean.Meta.setPostponed postponed) pure (DoResultPR.return a PUnit.unit) if a_1 = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.Term.throwStuckAtUniverseCnstr _do_jp y) fun ex => do liftM (Lean.Meta.setPostponed postponed) let y ← throw ex pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b

source

def Lean.Elab.Term.expandDeclId (currNamespace : Lean.Name) (currLevelNames : List Lean.Name) (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) :

Lean.Elab.TermElabM Lean.Elab.ExpandDeclIdResult

Equations

Lean.Elab.Term.expandDeclId currNamespace currLevelNames declId modifiers = do let r ← Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers let a ← read let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Elab.ExpandDeclIdResult := fun y => pure r if Lean.NameMap.contains a.sectionVars r.shortName = true then do let y ← Lean.throwError (Lean.toMessageData "invalid declaration name '" ++ Lean.toMessageData r.shortName ++ Lean.toMessageData "', there is a section variable with the same name") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.withoutModifyingStateWithInfoAndMessages {m : Type → Type u_1} {α : Type} [inst : MonadControlT Lean.Elab.TermElabM m] [inst : Monad m] (x : m α) :

m α

Equations

Lean.Elab.withoutModifyingStateWithInfoAndMessages x = controlAt Lean.Elab.TermElabM fun runInBase => Lean.Elab.Term.withoutModifyingStateWithInfoAndMessagesImpl (runInBase x)