The universe of propositions. Prop ≡ Sort 0.
Equations
A specific universe in Lean's infinite hierarchy of universes.
Equations
- Lean.Elab.Term.elabSort stx x = do let a ← Lean.Elab.Term.elabOptLevel (Lean.Syntax.getOp stx 1) pure (Lean.mkSort a)
A type universe. Type ≡ Type 0, Type u ≡ Sort (u + 1).
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A placeholder term, to be synthesized by unification.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
by tac constructs a term of the expected type by running the tactic(s) tac.
Equations
- One or more equations did not get rendered due to their size.
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 x 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
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.elabRawNatLit stx x = match Lean.Syntax.isNatLit? (Lean.Syntax.getOp stx 1) with | some val => pure (Lean.mkRawNatLit val) | none => Lean.Elab.throwIllFormedSyntax
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
A resolved name literal. Evaluates to the full name of the given constant if existent in the current context, or else fails.
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
open ... in e makes the given namespaces available in the term e.
Equations
- One or more equations did not get rendered due to their size.
set_option opt val in e sets the option opt to the value val in the term e.
Equations
- One or more equations did not get rendered due to their size.