Documentation

Init.Core

def inline {α : Sort u} (a : α) :
α
Equations
@[inline]
def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : αβφ) :
βαφ
Equations
@[simp]
theorem Function.const_apply {β : Sort u_1} {α : Sort u_2} {y : β} {x : α} :
Function.const α y x = y
@[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)
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.

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

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

@[extern lean_thunk_get_own]
def Thunk.get {α : Type u_1} (x : Thunk α) :
α
Equations
@[inline]
def Thunk.map {α : Type u_1} {β : Type u_2} (f : αβ) (x : Thunk α) :
Equations
@[inline]
def Thunk.bind {α : Type u_1} {β : Type u_2} (x : Thunk α) (f : αThunk β) :
Equations
@[simp]
theorem Thunk.sizeOf_eq {α : Type u_1} [inst : SizeOf α] (a : Thunk α) :
structure Iff (a : Prop) (b : Prop) :
Prop
  • intro :: (
    • mp : ab
    • mpr : (a : b) → a
  • )
inductive Sum (α : Type u) (β : Type v) :
Type (max u v)
  • inl: {α : Type u} → {β : Type v} → αα β
  • inr: {α : Type u} → {β : Type v} → βα β
inductive PSum (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • inl: {α : Sort u} → {β : Sort v} → αα ⊕' β
  • inr: {α : Sort u} → {β : Sort v} → βα ⊕' β
@[unbox]
structure Sigma {α : Type u} (β : αType v) :
Type (max u v)
  • fst : α
  • snd : β fst
structure PSigma {α : Sort u} (β : αSort v) :
Sort (max (max 1 u) v)
  • fst : α
  • snd : β fst
inductive Exists {α : Sort u} (p : αProp) :
Prop
  • intro: ∀ {α : Sort u} {p : αProp} (w : α), p wExists p
inductive ForInStep (α : Type u) :
Type u
  • done: {α : Type u} → αForInStep α
  • yield: {α : Type u} → αForInStep α
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
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
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 α β σ
inductive DoResultPR (α : Type u) (β : Type u) (σ : Type u) :
Type u
  • pure: {α β σ : Type u} → ασDoResultPR α β σ
  • return: {α β σ : Type u} → βσDoResultPR α β σ
inductive DoResultBC (σ : Type u) :
Type u
inductive DoResultSBC (α : Type u) (σ : Type u) :
Type u
  • pureReturn: {α σ : Type u} → ασDoResultSBC α σ
  • break: {α σ : Type u} → σDoResultSBC α σ
  • continue: {α σ : Type u} → σDoResultSBC α σ
class HasEquiv (α : Sort u) :
Sort (max u (v + 1))
  • Equiv : ααSort v
Instances
structure Task (α : Type u) :
Type u
  • pure :: (
    • get : α
  • )
instance instInhabitedTask :
{a : Type u_1} → [inst : Inhabited a] → Inhabited (Task a)
Equations
  • instInhabitedTask = { default := { get := default } }
@[inline]
abbrev Task.Priority :
Type
Equations

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

Equations

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.

@[noinline, extern lean_task_spawn]
def Task.spawn {α : Type u} (fn : Unitα) (prio : optParam Task.Priority Task.Priority.default) :
Task α
Equations
@[noinline, extern lean_task_map]
def Task.map {α : Type u} {β : Type v} (f : αβ) (x : Task α) (prio : optParam Task.Priority Task.Priority.default) :
Task β
Equations
@[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
structure NonScalar :
Type
inductive PNonScalar :
Type u
@[simp]
theorem Nat.add_zero (n : Nat) :
n + 0 = n
theorem optParam_eq (α : Sort u) (default : α) :
optParam α default = α
@[extern c inline "#1 || #2"]
def strictOr (b₁ : Bool) (b₂ : Bool) :
Equations
@[extern c inline "#1 && #2"]
def strictAnd (b₁ : Bool) (b₂ : Bool) :
Equations
@[inline]
def bne {α : Type u} [inst : BEq α] (a : α) (b : α) :
Equations
theorem eq_of_beq {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] {a : α} {b : α} (h : (a == b) = true) :
a = b
noncomputable def implies (a : Prop) (b : Prop) :
Prop
Equations
theorem implies.trans {p : Prop} {q : Prop} {r : Prop} (h₁ : implies p q) (h₂ : implies q r) :
noncomputable def trivial :
Equations
theorem mt {a : Prop} {b : Prop} (h₁ : ab) (h₂ : ¬b) :
theorem not_not_intro {p : Prop} (h : p) :
theorem proofIrrel {a : Prop} (h₁ : a) (h₂ : a) :
h₁ = h₂
theorem id.def {α : Sort u} (a : α) :
id a = a
@[macroInline]
def Eq.mp {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
β
Equations
@[macroInline]
def Eq.mpr {α : Sort u} {β : Sort u} (h : α = β) (b : β) :
α
Equations
theorem Eq.substr {α : Sort u} {p : αProp} {a : α} {b : α} (h₁ : b = a) (h₂ : p a) :
p b
theorem cast_eq {α : Sort u} (h : α = α) (a : α) :
cast h a = a
noncomputable def Ne {α : Sort u} (a : α) (b : α) :
Prop
Equations
theorem Ne.intro {α : Sort u} {a : α} {b : α} (h : a = bFalse) :
a b
theorem Ne.elim {α : Sort u} {a : α} {b : α} (h : a b) :
a = bFalse
theorem Ne.irrefl {α : Sort u} {a : α} (h : a a) :
theorem Ne.symm {α : Sort u} {a : α} {b : α} (h : a b) :
b a
theorem false_of_ne {α : Sort u} {a : α} :
a aFalse
theorem ne_false_of_self {p : Prop} :
pp False
theorem ne_true_of_not {p : Prop} :
¬pp True
theorem Bool.of_not_eq_true {b : Bool} :
¬b = trueb = false
theorem Bool.of_not_eq_false {b : Bool} :
¬b = falseb = true
theorem ne_of_beq_false {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] {a : α} {b : α} (h : (a == b) = false) :
a b
theorem beq_false_of_ne {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] {a : α} {b : α} (h : a b) :
(a == b) = false
theorem HEq.ndrec {α : Sort u2} {a : α} {motive : {β : Sort u2} → βSort u1} (m : motive α a) {β : Sort u2} {b : β} (h : HEq a b) :
motive β b
theorem HEq.ndrecOn {α : Sort u2} {a : α} {motive : {β : Sort u2} → βSort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive α a) :
motive β b
theorem HEq.elim {α : Sort u} {a : α} {p : αSort v} {b : α} (h₁ : HEq a b) (h₂ : p a) :
p b
theorem HEq.subst {α : Sort u} {β : Sort u} {a : α} {b : β} {p : (T : Sort u) → TProp} (h₁ : HEq a b) (h₂ : p α a) :
p β b
theorem HEq.symm {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
HEq b a
theorem heq_of_eq {α : Sort u} {a : α} {a' : α} (h : a = a') :
HEq a a'
theorem HEq.trans {α : Sort u} {β : Sort u} {φ : Sort u} {a : α} {b : β} {c : φ} (h₁ : HEq a b) (h₂ : HEq b c) :
HEq a c
theorem heq_of_heq_of_eq {α : Sort u} {β : Sort u} {a : α} {b : β} {b' : β} (h₁ : HEq a b) (h₂ : b = b') :
HEq a b'
theorem heq_of_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {a' : α} {b : β} (h₁ : a = a') (h₂ : HEq a' b) :
HEq a b
noncomputable def type_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
α = β
Equations
theorem eqRec_heq {α : Sort u} {φ : αSort v} {a : α} {a' : α} (h : a = a') (p : φ a) :
HEq (Eq.recOn h p) p
theorem heq_of_eqRec_eq {α : Sort u} {β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : h₁a = b) :
HEq a b
theorem cast_heq {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
HEq (cast h a) a
theorem iff_iff_implies_and_implies (a : Prop) (b : Prop) :
(a b) (ab) ((a : b) → a)
theorem Iff.refl (a : Prop) :
a a
theorem Iff.rfl {a : Prop} :
a a
theorem Iff.trans {a : Prop} {b : Prop} {c : Prop} (h₁ : a b) (h₂ : b c) :
a c
theorem Iff.symm {a : Prop} {b : Prop} (h : a b) :
b a
theorem Iff.comm {a : Prop} {b : Prop} :
(a b) (b a)
theorem Exists.elim {α : Sort u} {p : αProp} {b : Prop} (h₁ : ∃ x, p x) (h₂ : (a : α) → p ab) :
b
@[inline]
def toBoolUsing {p : Prop} (d : Decidable p) :
Equations

Similar to decide, but uses an explicit instance

theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) :
theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) :
p
theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) :
@[macroInline]
def Decidable.byCases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : pq) (h2 : ¬pq) :
q
Equations
theorem Decidable.em (p : Prop) [inst : Decidable p] :
p ¬p
theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬pFalse) :
p
theorem Decidable.of_not_not {p : Prop} [inst : Decidable p] :
¬¬pp
theorem Decidable.not_and_iff_or_not (p : Prop) (q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] :
¬(p q) ¬p ¬q
@[inline]
def decidable_of_decidable_of_iff {p : Prop} {q : Prop} [inst : Decidable p] (h : p q) :
Equations
@[inline]
def decidable_of_decidable_of_eq {p : Prop} {q : Prop} [hp : Decidable p] (h : p = q) :
Equations
@[macroInline]
instance instDecidableForAll {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] :
Decidable (pq)
Equations
instance instDecidableIff {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] :
Equations
theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : α} {e : α} :
(if c then t else e) = t
theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : α} {e : α} :
(if c then t else e) = e
theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : cα} {e : ¬cα} :
dite c t e = t hc
theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : cα} {e : ¬cα} :
dite c t e = e hnc
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
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
instance instDecidableDitePropNot {c : Prop} {t : cProp} {e : ¬cProp} [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
@[inline]
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : αβ) (P : Sort w) (x : α) (y : α) :
Sort w
Equations
@[inline]
abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : αβ) {P : Sort w} {x : α} {y : α} (h : x = y) :
Equations
instance instInhabitedProp :
Equations
instance instInhabitedForInStep :
{a : Type u_1} → [inst : Inhabited a] → Inhabited (ForInStep a)
Equations
Equations
Equations
theorem nonempty_of_exists {α : Sort u} {p : αProp} :
(∃ x, p x) → Nonempty α
noncomputable def Subsingleton.elim {α : Sort u} [h : Subsingleton α] (a : α) (b : α) :
a = b
Equations
noncomputable def Subsingleton.helim {α : Sort u} {β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) :
HEq a b
Equations
noncomputable instance instSubsingleton (p : Prop) :
Equations
theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : pSort u} {h₂ : ¬pSort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :
structure Equivalence {α : Sort u} (r : ααProp) :
Prop
  • refl : (x : α) → r x x
  • symm : {x y : α} → r x yr y x
  • trans : {x y z : α} → r x yr y zr x z
noncomputable def emptyRelation {α : Sort u} :
ααProp
Equations
noncomputable def Subrelation {α : Sort u} (q : ααProp) (r : ααProp) :
Prop
Equations
noncomputable def InvImage {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) :
ααProp
Equations
  • InvImage r f a₁ a₂ = r (f a₁) (f a₂)
inductive TC {α : Sort u} (r : ααProp) :
ααProp
  • base: ∀ {α : Sort u} {r : ααProp} (a b : α), r a bTC r a b
  • trans: ∀ {α : Sort u} {r : ααProp} (a b c : α), TC r a bTC r b cTC r a c
noncomputable def Subtype.existsOfSubtype {α : Type u} {p : αProp} :
{ x // p x }∃ x, p x
Equations
theorem Subtype.eq {α : Type u} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1.val = a2.vala1 = a2
theorem Subtype.eta {α : Type u} {p : αProp} (a : { x // p x }) (h : p a.val) :
{ val := a.val, property := h } = a
instance Subtype.instInhabitedSubtype {α : Type u} {p : αProp} {a : α} (h : p a) :
Inhabited { x // p x }
Equations
instance Subtype.instDecidableEqSubtype {α : Type u} {p : αProp} [inst : DecidableEq α] :
DecidableEq { x // p x }
Equations
  • Subtype.instDecidableEqSubtype x x = match x with | { val := a, property := h₁ } => match x with | { val := b, property := h₂ } => if h : a = b then isTrue (_ : { val := a, property := h₁ } = { val := b, property := h₂ }) else isFalse (_ : { val := a, property := h₁ } = { val := b, property := h₂ }False)
instance Sum.inhabitedLeft {α : Type u} {β : Type v} [inst : Inhabited α] :
Inhabited (α β)
Equations
  • Sum.inhabitedLeft = { default := Sum.inl default }
instance Sum.inhabitedRight {α : Type u} {β : Type v} [inst : Inhabited β] :
Inhabited (α β)
Equations
  • Sum.inhabitedRight = { default := Sum.inr default }
instance instDecidableEqSum {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] :
Equations
instance instInhabitedProd {α : Type u_1} {β : Type u_2} [inst : Inhabited α] [inst : Inhabited β] :
Inhabited (α × β)
Equations
  • instInhabitedProd = { default := (default, default) }
instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] :
DecidableEq (α × β)
Equations
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₂ }
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 }
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
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)
theorem Prod.ext {α : Type u_1} {β : Type u_2} (p : α × β) :
(p.fst, p.snd) = p
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)
theorem ex_of_PSigma {α : Type u} {p : αProp} :
(x : α) ×' p x∃ x, p x
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₂ }
theorem PUnit.subsingleton (a : PUnit) (b : PUnit) :
a = b
theorem PUnit.eq_punit (a : PUnit) :
class Setoid (α : Sort u) :
Sort (max 1 u)
Instances
instance instHasEquiv {α : Sort u} [inst : Setoid α] :
Equations
  • instHasEquiv = { Equiv := Setoid.r }
theorem Setoid.refl {α : Sort u} [inst : Setoid α] (a : α) :
a a
theorem Setoid.symm {α : Sort u} [inst : Setoid α] {a : α} {b : α} (hab : a b) :
b a
theorem Setoid.trans {α : Sort u} [inst : Setoid α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
a c
axiom propext {a : Prop} {b : Prop} :
∀ (a : a b), a = b
theorem Eq.propIntro {a : Prop} {b : Prop} (h₁ : ab) (h₂ : (a : b) → a) :
a = b
instance instDecidableEqProp {p : Prop} {q : Prop} [d : Decidable (p q)] :
Decidable (p = q)
Equations
theorem Iff.subst {a : Prop} {b : Prop} {p : PropProp} (h₁ : a b) (h₂ : p a) :
p b
axiom Quot.sound {α : Sort u} {r : ααProp} {a : α} {b : α} :
∀ (a : r a b), Quot.mk r a = Quot.mk r b
theorem Quot.liftBeta {α : Sort u} {r : ααProp} {β : Sort v} (f : αβ) (c : ∀ (a b : α), r a bf a = f b) (a : α) :
Quot.lift f c (Quot.mk r a) = f a
theorem Quot.indBeta {α : Sort u} {r : ααProp} {motive : Quot rProp} (p : (a : α) → motive (Quot.mk r a)) (a : α) :
Quot.ind p (Quot.mk r a) = p a
@[inline]
abbrev Quot.liftOn {α : Sort u} {β : Sort v} {r : ααProp} (q : Quot r) (f : αβ) (c : ∀ (a b : α), r a bf a = f b) :
β
Equations
theorem Quot.inductionOn {α : Sort u} {r : ααProp} {motive : Quot rProp} (q : Quot r) (h : (a : α) → motive (Quot.mk r a)) :
motive q
theorem Quot.exists_rep {α : Sort u} {r : ααProp} (q : Quot r) :
∃ a, Quot.mk r a = q
@[macroInline]
def Quot.indep {α : Sort u} {r : ααProp} {motive : Quot rSort v} (f : (a : α) → motive (Quot.mk r a)) (a : α) :
PSigma motive
Equations
theorem Quot.indepCoherent {α : Sort u} {r : ααProp} {motive : Quot rSort 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
theorem Quot.liftIndepPr1 {α : Sort u} {r : ααProp} {motive : Quot rSort 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 bQuot.indep f a = Quot.indep f b) q).fst = q
@[inline]
abbrev Quot.rec {α : Sort u} {r : ααProp} {motive : Quot rSort 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
@[inline]
abbrev Quot.recOn {α : Sort u} {r : ααProp} {motive : Quot rSort 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
@[inline]
abbrev Quot.recOnSubsingleton {α : Sort u} {r : ααProp} {motive : Quot rSort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :
motive q
Equations
@[inline]
abbrev Quot.hrecOn {α : Sort u} {r : ααProp} {motive : Quot rSort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : ∀ (a b : α), r a bHEq (f a) (f b)) :
motive q
Equations
noncomputable def Quotient {α : Sort u} (s : Setoid α) :
Sort u
Equations
@[inline]
def Quotient.mk {α : Sort u} (s : Setoid α) (a : α) :
Equations
def Quotient.mk' {α : Sort u} [s : Setoid α] (a : α) :
Equations
noncomputable def Quotient.sound {α : Sort u} {s : Setoid α} {a : α} {b : α} :
∀ (a : a b), Quotient.mk s a = Quotient.mk s b
Equations
@[inline]
abbrev Quotient.lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : αβ) :
(∀ (a b : α), a bf a = f b) → Quotient sβ
Equations
theorem Quotient.ind {α : Sort u} {s : Setoid α} {motive : Quotient sProp} :
((a : α) → motive (Quotient.mk s a)) → (q : Quot Setoid.r) → motive q
@[inline]
abbrev Quotient.liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : αβ) (c : ∀ (a b : α), a bf a = f b) :
β
Equations
theorem Quotient.inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient sProp} (q : Quotient s) (h : (a : α) → motive (Quotient.mk s a)) :
motive q
theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) :
∃ a, Quotient.mk s a = q
@[inline]
def Quotient.rec {α : Sort u} {s : Setoid α} {motive : Quotient sSort 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
@[inline]
abbrev Quotient.recOn {α : Sort u} {s : Setoid α} {motive : Quotient sSort 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
@[inline]
abbrev Quotient.recOnSubsingleton {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))] (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) :
motive q
Equations
@[inline]
abbrev Quotient.hrecOn {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (c : ∀ (a b : α), a bHEq (f a) (f b)) :
motive q
Equations
@[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
@[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
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₂
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₂
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₃
theorem Quotient.exact {α : Sort u} {s : Setoid α} {a : α} {b : α} :
∀ (a : Quotient.mk s a = Quotient.mk s b), a b
@[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
instance instDecidableEqQuotient {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a b)] :
Equations
noncomputable def Function.Equiv {α : Sort u} {β : αSort v} (f₁ : (x : α) → β x) (f₂ : (x : α) → β x) :
Prop
Equations
theorem Function.Equiv.refl {α : Sort u} {β : αSort v} (f : (x : α) → β x) :
theorem Function.Equiv.symm {α : Sort u} {β : αSort v} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} :
Function.Equiv f₁ f₂Function.Equiv f₂ f₁
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₃
theorem Function.Equiv.isEquivalence (α : Sort u) (β : αSort v) :
Equivalence Function.Equiv
theorem funext {α : Sort u} {β : αSort v} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} (h : ∀ (x : α), f₁ x = f₂ x) :
f₁ = f₂
noncomputable instance instSubsingletonForAll {α : Sort u} {β : αSort v} [inst : ∀ (a : α), Subsingleton (β a)] :
Subsingleton ((a : α) → β a)
Equations
noncomputable def Squash (α : Type u) :
Type u
Equations
def Squash.mk {α : Type u} (x : α) :
Equations
theorem Squash.ind {α : Type u} {motive : Squash αProp} (h : (a : α) → motive (Squash.mk a)) (q : Squash α) :
motive q
@[inline]
def Squash.lift {α : Type u_1} {β : Sort u_2} [inst : Subsingleton β] (s : Squash α) (f : αβ) :
β
Equations
class Antisymm {α : Sort u} (r : ααProp) :
Type
  • antisymm : ∀ {a b : α}, r a br b aa = b
Instances
constant Lean.reduceBool (b : Bool) :

When the kernel tries to reduce a term Lean.reduceBoolc, 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.reduceBoolt where t is a term not containing free variables. The frontend automatically declares a fresh auxiliary constant c and replaces the term with Lean.reduceBoolc. 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.

constant Lean.reduceNat (n : 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).

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