Documentation

Init.Core

source
def inline {α : Sort u} (a : α) :
α
Equations
source
@[inline]
def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) :
β → α → φ
Equations
source
@[simp]
theorem Function.const_apply {β : Sort u_1} {α : Sort u_2} {y : β} {x : α} :
Function.const α y x = y
source
@[simp]
theorem Function.comp_apply {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α} :
Function.comp f g x = f (g x)
source
structure Thunk (α : Type u) :
Type u

Thunks are "lazy" values that are evaluated when first accessed using Thunk.get/map/bind. The value is then stored and not recomputed for all further accesses.

source
@[extern lean_thunk_pure]
def Thunk.pure {α : Type u_1} (a : α) :
Thunk α

Store a value in a thunk. Note that the value has already been computed, so there is no laziness.

Equations
source
@[extern lean_thunk_get_own]
def Thunk.get {α : Type u_1} (x : Thunk α) :
α
Equations
source
@[inline]
def Thunk.map {α : Type u_1} {β : Type u_2} (f : α → β) (x : Thunk α) :
Thunk β
Equations
source
@[inline]
def Thunk.bind {α : Type u_1} {β : Type u_2} (x : Thunk α) (f : α → Thunk β) :
Thunk β
Equations
source
@[simp]
theorem Thunk.sizeOf_eq {α : Type u_1} [inst : SizeOf α] (a : Thunk α) :
sizeOf a = 1 + sizeOf (Thunk.get a)
source
structure Iff (a : Prop) (b : Prop) :
Prop
  • intro :: (
    • mp : a → b
    • mpr : (a : b) → a
  • )
source
def «term_<->_»:
Lean.TrailingParserDescr
Equations
source
def «term_↔_»:
Lean.TrailingParserDescr
Equations
source
inductive Sum (α : Type u) (β : Type v) :
Type (max u v)
  • inl: {α : Type u} → {β : Type v} → α → α ⊕ β
  • inr: {α : Type u} → {β : Type v} → β → α ⊕ β
source
def «term_⊕_»:
Lean.TrailingParserDescr
Equations
source
inductive PSum (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • inl: {α : Sort u} → {β : Sort v} → α → α ⊕' β
  • inr: {α : Sort u} → {β : Sort v} → β → α ⊕' β
source
def «term_⊕'_»:
Lean.TrailingParserDescr
Equations
source
@[unbox]
structure Sigma {α : Type u} (β : α → Type v) :
Type (max u v)
  • fst : α
  • snd : β fst
source
structure PSigma {α : Sort u} (β : α → Sort v) :
Sort (max (max 1 u) v)
  • fst : α
  • snd : β fst
source
inductive Exists {α : Sort u} (p : α → Prop) :
Prop
  • intro: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
source
inductive ForInStep (α : Type u) :
Type u
source
class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) :
Type (max (max (max u (u₁ + 1)) u₂) v)
  • forIn : {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β
Instances
source
class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) :
Type (max (max (max u (u₁ + 1)) u₂) v)
  • forIn' : {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β
Instances
source
inductive DoResultPRBC (α : Type u) (β : Type u) (σ : Type u) :
Type u
  • pure: {α β σ : Type u} → α → σ → DoResultPRBC α β σ
  • return: {α β σ : Type u} → β → σ → DoResultPRBC α β σ
  • break: {α β σ : Type u} → σ → DoResultPRBC α β σ
  • continue: {α β σ : Type u} → σ → DoResultPRBC α β σ
source
inductive DoResultPR (α : Type u) (β : Type u) (σ : Type u) :
Type u
  • pure: {α β σ : Type u} → α → σ → DoResultPR α β σ
  • return: {α β σ : Type u} → β → σ → DoResultPR α β σ
source
inductive DoResultBC (σ : Type u) :
Type u
source
inductive DoResultSBC (α : Type u) (σ : Type u) :
Type u
  • pureReturn: {α σ : Type u} → α → σ → DoResultSBC α σ
  • break: {α σ : Type u} → σ → DoResultSBC α σ
  • continue: {α σ : Type u} → σ → DoResultSBC α σ
source
class HasEquiv (α : Sort u) :
Sort (max u (v + 1))
  • Equiv : α → α → Sort v
Instances
source
def «term_≈_»:
Lean.TrailingParserDescr
Equations
source
class EmptyCollection (α : Type u) :
Type u
  • emptyCollection : α
Instances
source
def «term{}»:
Lean.ParserDescr
Equations
source
def «term∅»:
Lean.ParserDescr
Equations
source
structure Task (α : Type u) :
Type u
  • pure :: (
    • get : α
  • )
source
instance instInhabitedTask:
{a : Type u_1} → [inst : Inhabited a] → Inhabited (Task a)
Equations
  • instInhabitedTask = { default := { get := default } }
source
@[inline]
abbrev Task.Priority:
Type

Task priority. Tasks with higher priority will always be scheduled before ones with lower priority.

Equations
source
def Task.Priority.default:
Task.Priority
Equations
source
def Task.Priority.max:
Task.Priority
Equations
source
def Task.Priority.dedicated:
Task.Priority

Any priority higher than Task.Priority.max will result in the task being scheduled immediately on a dedicated thread. This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more non-dedicated workers than the number of cores to reduce context switches.

Equations
source
@[noinline, extern lean_task_spawn]
def Task.spawn {α : Type u} (fn : Unit → α) (prio : optParam Task.Priority Task.Priority.default) :
Task α
Equations
source
@[noinline, extern lean_task_map]
def Task.map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio : optParam Task.Priority Task.Priority.default) :
Task β
Equations
source
@[noinline, extern lean_task_bind]
def Task.bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio : optParam Task.Priority Task.Priority.default) :
Task β
Equations
source
structure NonScalar:
Type
source
inductive PNonScalar:
Type u
source
@[simp]
theorem Nat.add_zero (n : Nat) :
n + 0 = n
source
theorem optParam_eq (α : Sort u) (default : α) :
optParam α default = α
source
@[extern c inline "#1 || #2"]
def strictOr (b₁ : Bool) (b₂ : Bool) :
Bool
Equations
source
@[extern c inline "#1 && #2"]
def strictAnd (b₁ : Bool) (b₂ : Bool) :
Bool
Equations
source
@[inline]
def bne {α : Type u} [inst : BEq α] (a : α) (b : α) :
Bool
Equations
source
def «term_!=_»:
Lean.TrailingParserDescr
Equations
source
class LawfulBEq (α : Type u) [inst : BEq α] :
Prop
  • eq_of_beq : ∀ {a b : α}, (a == b) = true → a = b
  • rfl : ∀ {a : α}, (a == a) = true
Instances
source
instance instLawfulBEqBoolInstBEqInstDecidableEqBool:
LawfulBEq Bool
Equations
source
instance instLawfulBEqCharInstBEqInstDecidableEqChar:
LawfulBEq Char
Equations
source
instance instLawfulBEqStringInstBEqInstDecidableEqString:
LawfulBEq String
Equations
source
def implies (a : Prop) (b : Prop) :
Prop
Equations
source
theorem implies.trans {p : Prop} {q : Prop} {r : Prop} (h₁ : implies p q) (h₂ : implies q r) :
implies p r
source
def trivial:
True
Equations
source
theorem mt {a : Prop} {b : Prop} (h₁ : a → b) (h₂ : ¬b) :
¬a
source
theorem not_false:
¬False
source
theorem not_not_intro {p : Prop} (h : p) :
¬¬p
source
theorem proofIrrel {a : Prop} (h₁ : a) (h₂ : a) :
h₁ = h₂
source
theorem id.def {α : Sort u} (a : α) :
id a = a
source
@[macroInline]
def Eq.mp {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
β
Equations
source
@[macroInline]
def Eq.mpr {α : Sort u} {β : Sort u} (h : α = β) (b : β) :
α
Equations
source
theorem Eq.substr {α : Sort u} {p : α → Prop} {a : α} {b : α} (h₁ : b = a) (h₂ : p a) :
p b
source
theorem cast_eq {α : Sort u} (h : α = α) (a : α) :
cast h a = a
source
def Ne {α : Sort u} (a : α) (b : α) :
Prop
Equations
source
def «term_≠_»:
Lean.TrailingParserDescr
Equations
source
theorem Ne.intro {α : Sort u} {a : α} {b : α} (h : a = b → False) :
a ≠ b
source
theorem Ne.elim {α : Sort u} {a : α} {b : α} (h : a ≠ b) :
a = b → False
source
theorem Ne.irrefl {α : Sort u} {a : α} (h : a ≠ a) :
False
source
theorem Ne.symm {α : Sort u} {a : α} {b : α} (h : a ≠ b) :
b ≠ a
source
theorem false_of_ne {α : Sort u} {a : α} :
a ≠ a → False
source
theorem ne_false_of_self {p : Prop} :
p → p ≠ False
source
theorem ne_true_of_not {p : Prop} :
¬p → p ≠ True
source
theorem true_ne_false:
¬True = False
source
theorem Bool.of_not_eq_true {b : Bool} :
¬b = true → b = false
source
theorem Bool.of_not_eq_false {b : Bool} :
¬b = false → b = true
source
theorem ne_of_beq_false {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] {a : α} {b : α} (h : (a == b) = false) :
a ≠ b
source
theorem beq_false_of_ne {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] {a : α} {b : α} (h : a ≠ b) :
(a == b) = false
source
theorem HEq.ndrec {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive α a) {β : Sort u2} {b : β} (h : HEq a b) :
motive β b
source
theorem HEq.ndrecOn {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive α a) :
motive β b
source
theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) :
p b
source
theorem HEq.subst {α : Sort u} {β : Sort u} {a : α} {b : β} {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) :
p β b
source
theorem HEq.symm {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
HEq b a
source
theorem heq_of_eq {α : Sort u} {a : α} {a' : α} (h : a = a') :
HEq a a'
source
theorem HEq.trans {α : Sort u} {β : Sort u} {φ : Sort u} {a : α} {b : β} {c : φ} (h₁ : HEq a b) (h₂ : HEq b c) :
HEq a c
source
theorem heq_of_heq_of_eq {α : Sort u} {β : Sort u} {a : α} {b : β} {b' : β} (h₁ : HEq a b) (h₂ : b = b') :
HEq a b'
source
theorem heq_of_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {a' : α} {b : β} (h₁ : a = a') (h₂ : HEq a' b) :
HEq a b
source
def type_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
α = β
Equations
source
theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a : α} {a' : α} (h : a = a') (p : φ a) :
HEq (Eq.recOn h p) p
source
theorem heq_of_eqRec_eq {α : Sort u} {β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : h₁ ▸ a = b) :
HEq a b
source
theorem cast_heq {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
HEq (cast h a) a
source
theorem iff_iff_implies_and_implies (a : Prop) (b : Prop) :
(a ↔ b) ↔ (a → b) ∧ ((a : b) → a)
source
theorem Iff.refl (a : Prop) :
a ↔ a
source
theorem Iff.rfl {a : Prop} :
a ↔ a
source
theorem Iff.trans {a : Prop} {b : Prop} {c : Prop} (h₁ : a ↔ b) (h₂ : b ↔ c) :
a ↔ c
source
theorem Iff.symm {a : Prop} {b : Prop} (h : a ↔ b) :
b ↔ a
source
theorem Iff.comm {a : Prop} {b : Prop} :
(a ↔ b) ↔ (b ↔ a)
source
theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : ∃ x, p x) (h₂ : (a : α) → p a → b) :
b
source
theorem decide_true_eq_true (h : Decidable True) :
decide True = true
source
theorem decide_false_eq_false (h : Decidable False) :
decide False = false
source
@[inline]
def toBoolUsing {p : Prop} (d : Decidable p) :
Bool

Similar to decide, but uses an explicit instance

Equations
source
theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) :
toBoolUsing d = true
source
theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) :
p
source
theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) :
¬p
source
instance instDecidableTrue:
Decidable True
Equations
source
instance instDecidableFalse:
Decidable False
Equations
source
@[macroInline]
def Decidable.byCases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) :
q
Equations
source
theorem Decidable.em (p : Prop) [inst : Decidable p] :
p ∨ ¬p
source
theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) :
p
source
theorem Decidable.of_not_not {p : Prop} [inst : Decidable p] :
¬¬p → p
source
theorem Decidable.not_and_iff_or_not (p : Prop) (q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] :
¬(p ∧ q) ↔ ¬p ∨ ¬q
source
@[inline]
def decidable_of_decidable_of_iff {p : Prop} {q : Prop} [inst : Decidable p] (h : p ↔ q) :
Decidable q
Equations
source
@[inline]
def decidable_of_decidable_of_eq {p : Prop} {q : Prop} [hp : Decidable p] (h : p = q) :
Decidable q
Equations
source
@[macroInline]
instance instDecidableForAll {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] :
Decidable (p → q)
Equations
source
instance instDecidableIff {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] :
Decidable (p ↔ q)
Equations
source
theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : α} {e : α} :
(if c then t else e) = t
source
theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : α} {e : α} :
(if c then t else e) = e
source
theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :
dite c t e = t hc
source
theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :
dite c t e = e hnc
source
theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
(if x : c then t else e) = if c then t else e
source
instance instDecidableIteProp {c : Prop} {t : Prop} {e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] :
Decidable (if c then t else e)
Equations
  • instDecidableIteProp = match dC with | isTrue h => dT | isFalse h => dE
source
instance instDecidableDitePropNot {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : (h : c) → Decidable (t h)] [dE : (h : ¬c) → Decidable (e h)] :
Decidable (if h : c then t h else e h)
Equations
  • instDecidableDitePropNot = match dC with | isTrue hc => dT hc | isFalse hc => dE hc
source
@[inline]
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x : α) (y : α) :
Sort w
Equations
source
@[inline]
abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x : α} {y : α} (h : x = y) :
noConfusionTypeEnum f P x y
Equations
source
instance instInhabitedProp:
Inhabited Prop
Equations
source
instance instInhabitedPNonScalar:
Inhabited PNonScalar
Equations
source
instance instInhabitedTrue:
Inhabited True
Equations
source
instance instInhabitedForInStep:
{a : Type u_1} → [inst : Inhabited a] → Inhabited (ForInStep a)
Equations
source
instance instInhabitedNonScalar:
Inhabited NonScalar
Equations
source
theorem nonempty_of_exists {α : Sort u} {p : α → Prop} :
(∃ x, p x) → Nonempty α
source
class Subsingleton (α : Sort u) :
Prop
  • intro :: (
    • allEq : ∀ (a b : α), a = b
  • )
Instances
source
def Subsingleton.elim {α : Sort u} [h : Subsingleton α] (a : α) (b : α) :
a = b
Equations
source
def Subsingleton.helim {α : Sort u} {β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) :
HEq a b
Equations
source
instance instSubsingleton (p : Prop) :
Subsingleton p
Equations
source
instance instSubsingletonDecidable (p : Prop) :
Subsingleton (Decidable p)
Equations
source
theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :
Subsingleton (Decidable.casesOn h h₂ h₁)
source
structure Equivalence {α : Sort u} (r : α → α → Prop) :
Prop
  • refl : (x : α) → r x x
  • symm : {x y : α} → r x y → r y x
  • trans : {x y z : α} → r x y → r y z → r x z
source
def emptyRelation {α : Sort u} :
α → α → Prop
Equations
source
def Subrelation {α : Sort u} (q : α → α → Prop) (r : α → α → Prop) :
Prop
Equations
source
def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) :
α → α → Prop
Equations
source
inductive TC {α : Sort u} (r : α → α → Prop) :
α → α → Prop
  • base: ∀ {α : Sort u} {r : α → α → Prop} (a b : α), r a b → TC r a b
  • trans: ∀ {α : Sort u} {r : α → α → Prop} (a b c : α), TC r a b → TC r b c → TC r a c
source
instance Sum.inhabitedLeft {α : Type u} {β : Type v} [inst : Inhabited α] :
Inhabited (α ⊕ β)
Equations
  • Sum.inhabitedLeft = { default := Sum.inl default }
source
instance Sum.inhabitedRight {α : Type u} {β : Type v} [inst : Inhabited β] :
Inhabited (α ⊕ β)
Equations
  • Sum.inhabitedRight = { default := Sum.inr default }
source
instance instDecidableEqSum {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] :
DecidableEq (α ⊕ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance instInhabitedProd {α : Type u_1} {β : Type u_2} [inst : Inhabited α] [inst : Inhabited β] :
Inhabited (α × β)
Equations
  • instInhabitedProd = { default := (default, default) }
source
instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] :
DecidableEq (α × β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance instBEqProd {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : BEq β] :
BEq (α × β)
Equations
  • instBEqProd = { beq := fun x x_1 => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => a₁ == a₂ && b₁ == b₂ }
source
instance instLTProd {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
LT (α × β)
Equations
  • instLTProd = { lt := fun s t => s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd }
source
instance prodHasDecidableLt {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : DecidableEq α] [inst : DecidableEq β] [inst : (a b : α) → Decidable (a < b)] [inst : (a b : β) → Decidable (a < b)] (s : α × β) (t : α × β) :
Decidable (s < t)
Equations
source
theorem Prod.lt_def {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] (s : α × β) (t : α × β) :
(s < t) = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)
source
theorem Prod.ext {α : Type u_1} {β : Type u_2} (p : α × β) :
(p.fst, p.snd) = p
source
def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) :
α₁ × β₁ → α₂ × β₂
Equations
  • Prod.map f g _fun_discr = match _fun_discr with | (a, b) => (f a, g b)
source
theorem ex_of_PSigma {α : Type u} {p : α → Prop} :
(x : α) ×' p x → ∃ x, p x
source
theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ : α} {a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂) (h₂ : h₁ ▸ b₁ = b₂) :
{ fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
source
theorem PUnit.subsingleton (a : PUnit) (b : PUnit) :
a = b
source
theorem PUnit.eq_punit (a : PUnit) :
a = PUnit.unit
source
instance instSubsingletonPUnit:
Subsingleton PUnit
Equations
source
instance instInhabitedPUnit:
Inhabited PUnit
Equations
source
instance instDecidableEqPUnit:
DecidableEq PUnit
Equations
source
class Setoid (α : Sort u) :
Sort (max 1 u)
Instances
source
instance instHasEquiv {α : Sort u} [inst : Setoid α] :
HasEquiv α
Equations
  • instHasEquiv = { Equiv := Setoid.r }
source
theorem Setoid.refl {α : Sort u} [inst : Setoid α] (a : α) :
a ≈ a
source
theorem Setoid.symm {α : Sort u} [inst : Setoid α] {a : α} {b : α} (hab : a ≈ b) :
b ≈ a
source
theorem Setoid.trans {α : Sort u} [inst : Setoid α] {a : α} {b : α} {c : α} (hab : a ≈ b) (hbc : b ≈ c) :
a ≈ c
source
axiom propext {a : Prop} {b : Prop} :
∀ (a : a ↔ b), a = b
source
theorem Eq.propIntro {a : Prop} {b : Prop} (h₁ : a → b) (h₂ : (a : b) → a) :
a = b
source
instance instDecidableEqProp {p : Prop} {q : Prop} [d : Decidable (p ↔ q)] :
Decidable (p = q)
Equations
source
theorem Iff.subst {a : Prop} {b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) :
p b
source
axiom Quot.sound {α : Sort u} {r : α → α → Prop} {a : α} {b : α} :
∀ (a : r a b), Quot.mk r a = Quot.mk r b
source
theorem Quot.liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) (a : α) :
Quot.lift f c (Quot.mk r a) = f a
source
theorem Quot.indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : (a : α) → motive (Quot.mk r a)) (a : α) :
Quot.ind p (Quot.mk r a) = p a
source
@[inline]
abbrev Quot.liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) :
β
Equations
source
theorem Quot.inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r) (h : (a : α) → motive (Quot.mk r a)) :
motive q
source
theorem Quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) :
∃ a, Quot.mk r a = q
source
@[macroInline]
def Quot.indep {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (a : α) :
PSigma motive
Equations
source
theorem Quot.indepCoherent {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (a : α) (b : α) :
∀ (a : r a b), Quot.indep f a = Quot.indep f b
source
theorem Quot.liftIndepPr1 {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (q : Quot r) :
(Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).fst = q
source
@[inline]
abbrev Quot.rec {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (q : Quot r) :
motive q
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
abbrev Quot.recOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) :
motive q
Equations
source
@[inline]
abbrev Quot.recOnSubsingleton {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :
motive q
Equations
source
@[inline]
abbrev Quot.hrecOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : ∀ (a b : α), r a b → HEq (f a) (f b)) :
motive q
Equations
source
def Quotient {α : Sort u} (s : Setoid α) :
Sort u
Equations
source
@[inline]
def Quotient.mk {α : Sort u} (s : Setoid α) (a : α) :
Quotient s
Equations
source
def Quotient.mk' {α : Sort u} [s : Setoid α] (a : α) :
Quotient s
Equations
source
def Quotient.sound {α : Sort u} {s : Setoid α} {a : α} {b : α} :
∀ (a : a ≈ b), Quotient.mk s a = Quotient.mk s b
Equations
source
@[inline]
abbrev Quotient.lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) :
(∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β
Equations
source
theorem Quotient.ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} :
((a : α) → motive (Quotient.mk s a)) → (q : Quot Setoid.r) → motive q
source
@[inline]
abbrev Quotient.liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) :
β
Equations
source
theorem Quotient.inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s) (h : (a : α) → motive (Quotient.mk s a)) :
motive q
source
theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) :
∃ a, Quotient.mk s a = q
source
@[inline]
def Quotient.rec {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α), a ≈ b → (_ : Quotient.mk s a = Quotient.mk s b) ▸ f a = f b) (q : Quotient s) :
motive q
Equations
source
@[inline]
abbrev Quotient.recOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α), a ≈ b → (_ : Quotient.mk s a = Quotient.mk s b) ▸ f a = f b) :
motive q
Equations
source
@[inline]
abbrev Quotient.recOnSubsingleton {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))] (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) :
motive q
Equations
source
@[inline]
abbrev Quotient.hrecOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (c : ∀ (a b : α), a ≈ b → HEq (f a) (f b)) :
motive q
Equations
source
@[inline]
abbrev Quotient.lift₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
φ
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
abbrev Quotient.liftOn₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :
φ
Equations
source
theorem Quotient.ind₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
motive q₁ q₂
source
theorem Quotient.inductionOn₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
motive q₁ q₂
source
theorem Quotient.inductionOn₃ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ} {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : (a : α) → (b : β) → (c : φ) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)) :
motive q₁ q₂ q₃
source
theorem Quotient.exact {α : Sort u} {s : Setoid α} {a : α} {b : α} :
∀ (a : Quotient.mk s a = Quotient.mk s b), a ≈ b
source
@[inline]
abbrev Quotient.recOnSubsingleton₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC} [s : ∀ (a : α) (b : β), Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (g : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
motive q₁ q₂
Equations
source
instance instDecidableEqQuotient {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a ≈ b)] :
DecidableEq (Quotient s)
Equations
  • One or more equations did not get rendered due to their size.
source
def Function.Equiv {α : Sort u} {β : α → Sort v} (f₁ : (x : α) → β x) (f₂ : (x : α) → β x) :
Prop
Equations
source
theorem Function.Equiv.refl {α : Sort u} {β : α → Sort v} (f : (x : α) → β x) :
Function.Equiv f f
source
theorem Function.Equiv.symm {α : Sort u} {β : α → Sort v} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} :
Function.Equiv f₁ f₂ → Function.Equiv f₂ f₁
source
theorem Function.Equiv.trans {α : Sort u} {β : α → Sort v} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} {f₃ : (x : α) → β x} :
Function.Equiv f₁ f₂ → Function.Equiv f₂ f₃ → Function.Equiv f₁ f₃
source
theorem Function.Equiv.isEquivalence (α : Sort u) (β : α → Sort v) :
Equivalence Function.Equiv
source
theorem funext {α : Sort u} {β : α → Sort v} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} (h : ∀ (x : α), f₁ x = f₂ x) :
f₁ = f₂
source
instance instSubsingletonForAll {α : Sort u} {β : α → Sort v} [inst : ∀ (a : α), Subsingleton (β a)] :
Subsingleton ((a : α) → β a)
Equations
source
def Squash (α : Type u) :
Type u
Equations
source
def Squash.mk {α : Type u} (x : α) :
Squash α
Equations
source
theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : (a : α) → motive (Squash.mk a)) (q : Squash α) :
motive q
source
@[inline]
def Squash.lift {α : Type u_1} {β : Sort u_2} [inst : Subsingleton β] (s : Squash α) (f : α → β) :
β
Equations
source
instance instSubsingletonSquash {α : Type u} :
Subsingleton (Squash α)
Equations
source
class Antisymm {α : Sort u} (r : α → α → Prop) :
Type
  • antisymm : ∀ {a b : α}, r a b → r b a → a = b
Instances
source
opaque Lean.reduceBool (b : Bool) :
Bool

When the kernel tries to reduce a term Lean.reduceBool c, it will invoke the Lean interpreter to evaluate c. The kernel will not use the interpreter if c is not a constant. This feature is useful for performing proofs by reflection.

Remark: the Lean frontend allows terms of the from Lean.reduceBool t where t is a term not containing free variables. The frontend automatically declares a fresh auxiliary constant c and replaces the term with Lean.reduceBool c. The main motivation is that the code for t will be pre-compiled.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your developement using external checkers.

Recall that the compiler trusts the correctness of all [implementedBy ...] and [extern ...] annotations. If an extern function is executed, then the trusted code base will also include the implementation of the associated foreign function.

source
opaque Lean.reduceNat (n : Nat) :
Nat

Similar to Lean.reduceBool for closed Nat terms.

Remark: we do not have plans for supporting a generic reduceValue {α} (a : α) : α := a. The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression. We believe Lean.reduceBool enables most interesting applications (e.g., proof by reflection).

source
axiom Lean.ofReduceBool (a : Bool) (b : Bool) (h : Lean.reduceBool a = b) :
a = b
source
axiom Lean.ofReduceNat (a : Nat) (b : Nat) (h : Lean.reduceNat a = b) :
a = b
source
class Lean.IsAssociative {α : Sort u} (op : α → α → α) :
Type
  • assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
Instances
    source
    class Lean.IsCommutative {α : Sort u} (op : α → α → α) :
    Type
    • comm : ∀ (a b : α), op a b = op b a
    Instances
      source
      class Lean.IsIdempotent {α : Sort u} (op : α → α → α) :
      Type
      • idempotent : ∀ (x : α), op x x = x
      Instances
        source
        class Lean.IsNeutral {α : Sort u} (op : α → α → α) (neutral : α) :
        Type
        • left_neutral : ∀ (a : α), op neutral a = a
        • right_neutral : ∀ (a : α), op a neutral = a
        Instances