def Lean.Elab.Term.elabProp : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabSort : Lean.Elab.Term.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 : Lean.Elab.Term.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 : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabCompletion : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabHole : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabSyntheticHole : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabOmission : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabLetMVar : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabWaitIfTypeMVar : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabWaitIfTypeContainsMVar : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabWaitIfContainsMVar : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabByTactic : Lean.Elab.Term.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 ∘ Lean.format) "invalid 'by' tactic, expected type has not been provided")

def Lean.Elab.Term.elabNoImplicitLambda : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabBadCDot : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabStrLit : Lean.Elab.Term.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 : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabRawNatLit : Lean.Elab.Term.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 : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabCharLit : Lean.Elab.Term.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 : Lean.Elab.Term.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 : Lean.Elab.Term.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 : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabWithDeclName : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabTypeOf : Lean.Elab.Term.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 : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabEnsureExpectedType : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabClear : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabOpen : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabSetOption : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabWithAnnotateTerm : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabIncludeStr : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabNamedPatternErr : Lean.Elab.Term.TermElab

Equations

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