Documentation

Equations

• Lean.Elab.Term.elabProp x x = pure (Lean.mkSort Lean.levelZero)

Equations

• Lean.Elab.Term.elabSort stx x = do let a ← Lean.Elab.Term.elabOptLevel (Lean.Syntax.getOp stx 1) pure (Lean.mkSort a)

Equations

• Lean.Elab.Term.elabTypeStx stx x = do let a ← Lean.Elab.Term.elabOptLevel (Lean.Syntax.getOp stx 1) pure (Lean.mkSort (Lean.mkLevelSucc a))

Equations

• Lean.Elab.Term.elabPipeCompletion stx expectedType? = do let e ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 0) none true true let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Expr := fun y => Lean.throwErrorAt (Lean.Syntax.getOp stx 1) (Lean.toMessageData "invalid field notation, identifier or numeral expected") if Lean.Expr.isSorry e = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.Term.addDotCompletionInfo stx e expectedType? none _do_jp y

Equations

• Lean.Elab.Term.elabCompletion stx expectedType? = if Lean.Syntax.isIdent (Lean.Syntax.getOp stx 0) = true then do let s ← Lean.saveState tryCatch (do let e ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 0) none true true Lean.Elab.Term.addDotCompletionInfo stx e expectedType? none) fun x => do Lean.Elab.Term.SavedState.restore s false let a ← Lean.getLCtx Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.id stx (Lean.Syntax.getId (Lean.Syntax.getOp stx 0)) true a expectedType?) Lean.throwErrorAt (Lean.Syntax.getOp stx 1) (Lean.toMessageData "invalid field notation, identifier or numeral expected") else Lean.Elab.Term.elabPipeCompletion stx expectedType?

Equations

• Lean.Elab.Term.elabHole stx expectedType? = do let mvar ← liftM (Lean.Meta.mkFreshExprMVar expectedType? Lean.MetavarKind.natural Lean.Name.anonymous) Lean.Elab.Term.registerMVarErrorHoleInfo (Lean.Expr.mvarId! mvar) stx pure mvar

Equations

• Lean.Elab.Term.elabSyntheticHole stx expectedType? = let arg := Lean.Syntax.getOp stx 1; let userName := if Lean.Syntax.isIdent arg = true then Lean.Syntax.getId arg else Lean.Name.anonymous; let mkNewHole := fun x => do let mvar ← liftM (Lean.Meta.mkFreshExprMVar expectedType? Lean.MetavarKind.syntheticOpaque userName) Lean.Elab.Term.registerMVarErrorHoleInfo (Lean.Expr.mvarId! mvar) stx pure mvar; if Lean.Name.isAnonymous userName = true then mkNewHole () else do let mctx ← Lean.getMCtx match Lean.MetavarContext.findUserName? mctx userName with | none => mkNewHole () | some mvarId => let mvar := Lean.mkMVar mvarId; do let mvarDecl ← Lean.Elab.Term.getMVarDecl mvarId let lctx ← Lean.getLCtx if Lean.LocalContext.isSubPrefixOf mvarDecl.lctx lctx = true then pure mvar else match Lean.MetavarContext.getExprAssignment? mctx mvarId with | some val => do let val ← liftM (Lean.Meta.instantiateMVars val) if Lean.MetavarContext.isWellFormed mctx lctx val = true then pure val else Lean.Meta.withLCtx mvarDecl.lctx mvarDecl.localInstances (Lean.throwError (Lean.toMessageData "synthetic hole has already been defined and assigned to value incompatible with the current context" ++ Lean.toMessageData (Lean.indentExpr val) ++ Lean.toMessageData "")) | none => if Lean.MetavarContext.isDelayedAssigned mctx mvarId = true then Lean.throwError (Lean.toMessageData "synthetic hole has already beend defined and delayed assigned with an incompatible local context") else if Lean.LocalContext.isSubPrefixOf lctx mvarDecl.lctx = true then do let mvarNew ← mkNewHole () Lean.modifyMCtx fun mctx => Lean.MetavarContext.assignExpr mctx mvarId mvarNew pure mvarNew else Lean.throwError (Lean.toMessageData "synthetic hole has already been defined with an incompatible local context")

Equations

• Lean.Elab.Term.elabLetMVar stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.letMVar = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; let discr_5 := Lean.Syntax.getArg discr 4; let discr_6 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; let b := discr; let e := discr_5; let n := discr_3; do let a ← Lean.getMCtx match Lean.MetavarContext.findUserName? a (Lean.Syntax.getId n) with | some x => Lean.throwError (Lean.toMessageData "invalid 'let_mvar%', metavariable '?" ++ Lean.toMessageData (Lean.Syntax.getId n) ++ Lean.toMessageData "' has already been used") | none => do let e ← Lean.Elab.Term.elabTerm e none true true let a ← liftM (Lean.Meta.inferType e) let mvar ← liftM (Lean.Meta.mkFreshExprMVar (some a) Lean.MetavarKind.syntheticOpaque (Lean.Syntax.getId n)) liftM (Lean.Meta.assignExprMVar (Lean.Expr.mvarId! mvar) e) let a ← Lean.Elab.Term.elabTerm b expectedType? true true pure (Lean.Elab.Term.mkSaveInfoAnnotation a) else let discr := stx; Lean.Elab.throwUnsupportedSyntax

Equations

• Lean.Elab.Term.elabWaitIfTypeMVar stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.waitIfTypeMVar = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let b := discr; let n := discr_3; do let a ← liftM (Lean.Elab.Term.getMVarFromUserName n) let a ← liftM (Lean.Meta.inferType a) Lean.Elab.Term.tryPostponeIfMVar a Lean.Elab.Term.elabTerm b expectedType? true true else let discr := stx; Lean.Elab.throwUnsupportedSyntax

Equations

• Lean.Elab.Term.elabWaitIfTypeContainsMVar stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.waitIfTypeContainsMVar = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let b := discr; let n := discr_3; do let a ← liftM (Lean.Elab.Term.getMVarFromUserName n) let a ← liftM (Lean.Meta.inferType a) let a ← liftM (Lean.Meta.instantiateMVars a) let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => Lean.Elab.Term.elabTerm b expectedType? true true if Lean.Expr.hasExprMVar a = true then do let y ← Lean.Elab.Term.tryPostpone _do_jp y else do let y ← pure PUnit.unit _do_jp y else let discr := stx; Lean.Elab.throwUnsupportedSyntax

Equations

• Lean.Elab.Term.elabWaitIfContainsMVar stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.waitIfContainsMVar = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let b := discr; let n := discr_3; do let a ← liftM (Lean.Elab.Term.getMVarFromUserName n) let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => Lean.Elab.Term.elabTerm b expectedType? true true if Lean.Expr.hasExprMVar a = true then do let y ← Lean.Elab.Term.tryPostpone _do_jp y else do let y ← pure PUnit.unit _do_jp y else let discr := stx; Lean.Elab.throwUnsupportedSyntax

Equations

• Lean.Elab.Term.elabByTactic stx expectedType? = match expectedType? with | some expectedType => Lean.Elab.Term.mkTacticMVar expectedType stx | none => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format "invalid 'by' tactic, expected type has not been provided")

Equations

• Lean.Elab.Term.elabNoImplicitLambda stx expectedType? = Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 1) (Lean.Elab.Term.mkNoImplicitLambdaAnnotation <$> expectedType?) true true

Equations

• Lean.Elab.Term.elabBadCDot stx x = Lean.throwError (Lean.toMessageData "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)")

Equations

• Lean.Elab.Term.elabStrLit stx x = match Lean.Syntax.isStrLit? stx with | some val => pure (Lean.mkStrLit val) | none => Lean.Elab.throwIllFormedSyntax

Equations

• Lean.Elab.Term.elabNumLit stx expectedType? = let _do_jp := fun val => do let typeMVar ← Lean.Elab.Term.mkFreshTypeMVarFor expectedType? let u ← liftM (Lean.Meta.getDecLevel typeMVar) let mvar ← Lean.Elab.Term.mkInstMVar (Lean.mkApp2 (Lean.mkConst `OfNat [u]) typeMVar (Lean.mkRawNatLit val)) let r : Lean.Expr := Lean.mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar (Lean.mkRawNatLit val) mvar Lean.Elab.Term.registerMVarErrorImplicitArgInfo (Lean.Expr.mvarId! mvar) stx r pure r; match Lean.Syntax.isNatLit? stx with | some val => do let y ← pure val _do_jp y | none => do let y ← Lean.Elab.throwIllFormedSyntax _do_jp y

Equations

• Lean.Elab.Term.elabRawNatLit stx expectedType? = match Lean.Syntax.isNatLit? (Lean.Syntax.getOp stx 1) with | some val => pure (Lean.mkRawNatLit val) | none => Lean.Elab.throwIllFormedSyntax

Equations

• Lean.Elab.Term.elabScientificLit stx expectedType? = match Lean.Syntax.isScientificLit? stx with | none => Lean.Elab.throwIllFormedSyntax | some (m, sign, e) => do let typeMVar ← Lean.Elab.Term.mkFreshTypeMVarFor expectedType? let u ← liftM (Lean.Meta.getDecLevel typeMVar) let mvar ← Lean.Elab.Term.mkInstMVar (Lean.mkApp (Lean.mkConst `OfScientific [u]) typeMVar) let r : Lean.Expr := Lean.mkApp5 (Lean.mkConst `OfScientific.ofScientific [u]) typeMVar mvar (Lean.mkRawNatLit m) (Lean.toExpr sign) (Lean.mkRawNatLit e) Lean.Elab.Term.registerMVarErrorImplicitArgInfo (Lean.Expr.mvarId! mvar) stx r pure r

Equations

• Lean.Elab.Term.elabCharLit stx x = match Lean.Syntax.isCharLit? stx with | some val => pure (Lean.mkApp (Lean.mkConst `Char.ofNat) (Lean.mkRawNatLit (Char.toNat val))) | none => Lean.Elab.throwIllFormedSyntax

Equations

• Lean.Elab.Term.elabQuotedName stx x = match Lean.Syntax.isNameLit? (Lean.Syntax.getOp stx 0) with | some val => pure (Lean.toExpr val) | none => Lean.Elab.throwIllFormedSyntax

Equations

• Lean.Elab.Term.elabDoubleQuotedName stx x = do let a ← Lean.Elab.resolveGlobalConstNoOverloadWithInfo (Lean.Syntax.getOp stx 2) pure (Lean.toExpr a)

Equations

• Lean.Elab.Term.elabTypeOf stx x = do let a ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 1) none true true liftM (Lean.Meta.inferType a)

Equations

• Lean.Elab.Term.elabEnsureTypeOf stx expectedType? = match Lean.Syntax.isStrLit? (Lean.Syntax.getOp stx 2) with | none => Lean.Elab.throwIllFormedSyntax | some msg => do let refTerm ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 1) none true true let refTermType ← liftM (Lean.Meta.inferType refTerm) Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp stx 3) (some refTermType) true true (some msg)

Equations

• Lean.Elab.Term.elabEnsureExpectedType stx expectedType? = match Lean.Syntax.isStrLit? (Lean.Syntax.getOp stx 1) with | none => Lean.Elab.throwIllFormedSyntax | some msg => Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp stx 2) expectedType? true true (some msg)

Equations

• Lean.Elab.Term.elabOpen stx expectedType? = tryFinally (do Lean.pushScope let openDecls ← Lean.Elab.elabOpenDecl (Lean.Syntax.getOp stx 1) withTheReader Lean.Core.Context (fun ctx => { options := ctx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) (Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 3) expectedType? true true)) Lean.popScope

Equations

• Lean.Elab.Term.elabSetOption stx expectedType? = do let options ← Lean.Elab.elabSetOption (Lean.Syntax.getOp stx 1) (Lean.Syntax.getOp stx 2) withTheReader Lean.Core.Context (fun ctx => { options := options, currRecDepth := ctx.currRecDepth, maxRecDepth := Lean.Option.get options Lean.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) (Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 4) expectedType? true true)