def Lean.Elab.Term.elabProp : TermElab

Equations

• Lean.Elab.Term.elabProp x✝¹ x✝ = pure (Lean.mkSort Lean.Level.zero)

def Lean.Elab.Term.elabSort : TermElab

Equations

• Lean.Elab.Term.elabSort stx x✝ = do let __do_lift ← Lean.Elab.Term.elabOptLevel✝ stx[1] pure (Lean.mkSort __do_lift)

def Lean.Elab.Term.elabTypeStx : TermElab

Equations

• Lean.Elab.Term.elabTypeStx stx x✝ = do let __do_lift ← Lean.Elab.Term.elabOptLevel✝ stx[1] pure (Lean.mkSort (Lean.mkLevelSucc __do_lift))

the method resolveName adds a completion point for it using the given expected type. Thus, we propagate the expected type if stx[0] is an identifier. It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case. Recall that if the name resolution fails a synthetic sorry is returned.

def Lean.Elab.Term.elabPipeCompletion : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabCompletion : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabHole : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabSyntheticHole : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabOmission : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabLetMVar : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabWaitIfTypeMVar : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabWaitIfTypeContainsMVar : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabWaitIfContainsMVar : TermElab

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Elab.Term.tactic.tryOnEmptyBy : Lean.Option Bool

def Lean.Elab.Term.isEmptyByBlock (stx : Syntax) : Bool

Returns true if stx is a by expression with an empty tactic body (not a parse error producing .missing). The structure is: node byTactic [atom "by", node tacticSeq [node tacticSeq1Indented [node null []]]]

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.shouldElabEmptyByAsTry (stx : Syntax) : TermElabM Bool

Returns true if all conditions are met for empty by to be elaborated as try?: the body is empty, the option is enabled, we are in an interactive (non-combinator) context, and the try? infrastructure (parser Lean.Parser.Tactic.tryTrace) is available — the latter matters when working on the prelude, before Init.Try is imported.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabByTacticCore : TermElab

Body of the byTactic term elaborator: registers a tactic mvar for the body, or errors when there's no expected type. Shared between elabByTactic and Lean.Elab.Tactic.Try's elabEmptyByAsTry so the two paths can't drift.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.elabByTacticCore stx none = do Lean.Elab.Term.tryPostpone Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) "invalid 'by' tactic, expected type has not been provided")

def Lean.Elab.Term.elabByTactic : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabNoImplicitLambda : TermElab

Equations

• Lean.Elab.Term.elabNoImplicitLambda stx expectedType? = Lean.Elab.Term.elabTerm stx[1] (Lean.Elab.Term.mkNoImplicitLambdaAnnotation <$> expectedType?)

def Lean.Elab.Term.elabBadCDot : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabStrLit : TermElab

Equations

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

def Lean.Elab.Term.elabNumLit : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabRawNatLit : TermElab

Equations

• Lean.Elab.Term.elabRawNatLit stx x✝ = match stx[1].isNatLit? with | some val => pure (Lean.mkRawNatLit val) | none => Lean.Elab.throwIllFormedSyntax

def Lean.Elab.Term.elabScientificLit : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabCharLit : TermElab

Equations

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

def Lean.Elab.Term.elabQuotedName : TermElab

Equations

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

def Lean.Elab.Term.elabDoubleQuotedName : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabDeclName : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabWithDeclName : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabTypeOf : TermElab

Equations

• Lean.Elab.Term.elabTypeOf stx x✝ = do let __do_lift ← Lean.Elab.Term.elabTerm stx[1] none liftM (Lean.Meta.inferType __do_lift)

def Lean.Elab.Term.elabEnsureTypeOf : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabEnsureExpectedType : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabValueOf : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabInferInstanceAs : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabClear : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabOpen : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabSetOption : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabWithAnnotateTerm : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabIncludeStr : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabNamedPatternErr : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabPrivateDecl : TermElab

Equations

• One or more equations did not get rendered due to their size.