def Lean.Elab.Term.elabProp : TermElab

Equations

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

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.

def Lean.Elab.Term.elabByTactic : TermElab

Equations

• Lean.Elab.Term.elabByTactic stx (some val) = Lean.Elab.Term.mkTacticMVar val stx Lean.Elab.Term.TacticMVarKind.term
• Lean.Elab.Term.elabByTactic 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.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

• Lean.Elab.Term.elabDoubleQuotedName stx x✝ = do let __do_lift ← liftM (Lean.Elab.realizeGlobalConstNoOverloadWithInfo stx[2]) pure (Lean.toExpr __do_lift)

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.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.