Equations
- Thunk.pure a = { fn := fun x => a }
Store a value in a thunk. Note that the value has already been computed, so there is no laziness.
Equations
- Thunk.bind x f = { fn := fun x => Thunk.get (f (Thunk.get x)) }
Equations
- «term_<->_» = Lean.ParserDescr.trailingNode `«term_<->_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <-> ") (Lean.ParserDescr.cat `term 21))
Equations
- «term_↔_» = Lean.ParserDescr.trailingNode `«term_↔_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 21))
Equations
- «term_⊕_» = Lean.ParserDescr.trailingNode `«term_⊕_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 30))
Equations
- «term_⊕'_» = Lean.ParserDescr.trailingNode `«term_⊕'_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕' ") (Lean.ParserDescr.cat `term 30))
- pure: {α β σ : Type u} → α → σ → DoResultPRBC α β σ
- return: {α β σ : Type u} → β → σ → DoResultPRBC α β σ
- break: {α β σ : Type u} → σ → DoResultPRBC α β σ
- continue: {α β σ : Type u} → σ → DoResultPRBC α β σ
- pure: {α β σ : Type u} → α → σ → DoResultPR α β σ
- return: {α β σ : Type u} → β → σ → DoResultPR α β σ
- break: {σ : Type u} → σ → DoResultBC σ
- continue: {σ : Type u} → σ → DoResultBC σ
- pureReturn: {α σ : Type u} → α → σ → DoResultSBC α σ
- break: {α σ : Type u} → σ → DoResultSBC α σ
- continue: {α σ : Type u} → σ → DoResultSBC α σ
- Equiv : α → α → Sort v
Instances
Equations
- «term_≈_» = Lean.ParserDescr.trailingNode `«term_≈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))
- emptyCollection : α
Equations
- «term{}» = Lean.ParserDescr.node `«term{}» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{") (Lean.ParserDescr.symbol "}"))
Equations
- «term∅» = Lean.ParserDescr.node `«term∅» 1024 (Lean.ParserDescr.symbol "∅")
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.
Equations
- Task.spawn fn prio = { get := fn () }
Equations
- «term_!=_» = Lean.ParserDescr.trailingNode `«term_!=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 51))
Instances
- List.instLawfulBEqListInstBEqList
- Nat.Linear.instLawfulBEqPolyCnstrInstBEqPolyCnstr
- Nat.instLawfulBEqNatInstBEqNat
- instLawfulBEqProdInstBEqProd
- instLawfulBEqBoolInstBEqInstDecidableEqBool
- instLawfulBEqStringInstBEqInstDecidableEqString
- instLawfulBEqCharInstBEqInstDecidableEqChar
- Int.instLawfulBEqIntInstBEqInstDecidableEqInt
Equations
- «term_≠_» = Lean.ParserDescr.trailingNode `«term_≠_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `term 51))
Equations
Equations
Equations
- Decidable.byCases h1 h2 = match dec with | isTrue h => h1 h | isFalse h => h2 h
Equations
- decidable_of_decidable_of_eq h = h ▸ hp
Equations
- instDecidableForAll = if hp : p then if hq : q then isTrue (instDecidableForAll.proof_1 hq) else isFalse (_ : (p → q) → False) else isTrue (instDecidableForAll.proof_3 hp)
Equations
- noConfusionTypeEnum f P x y = Decidable.casesOn (inst (f x) (f y)) (fun x => P) fun x => P → P
Equations
- noConfusionEnum f h = Decidable.casesOn (inst (f x) (f y)) (fun h' => False.elim (_ : False)) fun x x => x
Equations
- instInhabitedProp = { default := True }
Equations
- instInhabitedForInStep = { default := ForInStep.done default }
Equations
- instInhabitedPNonScalar = { default := PNonScalar.mk default }
Equations
- instInhabitedTrue = { default := True.intro }
Equations
- instInhabitedNonScalar = { default := { val := default } }
- intro :: (
- allEq : ∀ (a b : α), a = b
- )
Equations
Equations
Equations
- 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
Equations
- emptyRelation x x = False
Equations
- Subrelation q r = ({x y : α} → q x y → r x y)
Equations
- Subtype.instInhabitedSubtype h = { default := { val := a, property := h } }
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)
Equations
- instDecidableEqSum a b = match a, b with | Sum.inl a, Sum.inl b => if h : a = b then isTrue (_ : Sum.inl a = Sum.inl b) else isFalse (_ : Sum.inl a = Sum.inl b → False) | Sum.inr a, Sum.inr b => if h : a = b then isTrue (_ : Sum.inr a = Sum.inr b) else isFalse (_ : Sum.inr a = Sum.inr b → False) | Sum.inr val, Sum.inl val_1 => isFalse (_ : Sum.inr val = Sum.inl val_1 → Sum.noConfusionType False (Sum.inr val) (Sum.inl val_1)) | Sum.inl val, Sum.inr val_1 => isFalse (_ : Sum.inl val = Sum.inr val_1 → Sum.noConfusionType False (Sum.inl val) (Sum.inr val_1))
Equations
Equations
- prodHasDecidableLt x x = inferInstanceAs (Decidable (x.fst < x.fst ∨ x.fst = x.fst ∧ x.snd < x.snd))
Equations
Equations
- instInhabitedPUnit = { default := PUnit.unit }
Equations
- instDecidableEqPUnit a b = isTrue (_ : a = b)
- r : α → α → Prop
- iseqv : Equivalence r
Instances
Equations
- instHasEquiv = { Equiv := Setoid.r }
Equations
- Quot.liftOn q f c = Quot.lift f c q
Equations
- Quot.indep f a = { fst := Quot.mk r a, snd := f a }
Equations
- Quot.rec f h q = Eq.ndrecOn (_ : (Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).fst = q) (Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).snd
Equations
- Quot.hrecOn q f c = Quot.recOn q f (_ : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b)
Equations
- Quotient.mk s a = Quot.mk Setoid.r a
Equations
- Quotient.mk' a = Quotient.mk s a
Equations
Equations
- Quotient.lift f = Quot.lift f
Equations
- Quotient.liftOn q f c = Quot.liftOn q f c
Equations
- Quotient.rec f h q = Quot.rec f h q
Equations
- Quotient.recOn q f h = Quot.recOn q f h
Equations
Equations
- Quotient.hrecOn q f c = Quot.hrecOn q f c
Equations
- Quotient.lift₂ f c q₁ q₂ = Quotient.lift (fun a₁ => Quotient.lift (f a₁) (_ : ∀ (a b : β), a ≈ b → f a₁ a = f a₁ b) q₂) (_ : ∀ (a b : α), a ≈ b → (fun a₁ => Quotient.lift (f a₁) (fun a b => c a₁ a a₁ b (_ : a₁ ≈ a₁)) q₂) a = (fun a₁ => Quotient.lift (f a₁) (fun a b => c a₁ a a₁ b (_ : a₁ ≈ a₁)) q₂) b) q₁
Equations
- Quotient.liftOn₂ q₁ q₂ f c = Quotient.lift₂ f c q₁ q₂
Equations
- Quotient.recOnSubsingleton₂ q₁ q₂ g = Quot.recOnSubsingleton q₁ fun a => Quot.recOnSubsingleton q₂ fun a_1 => g a a_1
Equations
- instDecidableEqQuotient q₁ q₂ = Quotient.recOnSubsingleton₂ q₁ q₂ fun a₁ a₂ => match d a₁ a₂ with | isTrue h₁ => isTrue (_ : Quotient.mk s a₁ = Quotient.mk s a₂) | isFalse h₂ => isFalse (_ : Quotient.mk s a₁ = Quotient.mk s a₂ → False)
Equations
- Function.Equiv f₁ f₂ = ∀ (x : α), f₁ x = f₂ x
Equations
- Squash.lift s f = Quot.lift f (_ : ∀ (x x_1 : α), True → f x = f x_1) s
- antisymm : ∀ {a b : α}, r a b → r b a → a = b
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.
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).
- assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
Instances
- comm : ∀ (a b : α), op a b = op b a
Instances
- idempotent : ∀ (x : α), op x x = x