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

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

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?) true true

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

Equations

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

def Lean.Elab.Term.elabStrLit : Lean.Elab.Term.TermElab

Equations

• Lean.Elab.Term.elabStrLit stx x = match Lean.Syntax.isStrLit? stx 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 Lean.Syntax.isNatLit? stx[1] 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

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

def Lean.Elab.Term.elabQuotedName : Lean.Elab.Term.TermElab

Equations

• Lean.Elab.Term.elabQuotedName stx x = match Lean.Syntax.isNameLit? stx[0] 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 ← Lean.Elab.resolveGlobalConstNoOverloadWithInfo stx[2] none 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 true true 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.