Lean core references

Every Lean core declaration referred to directly by this project’s own code, grouped by the module it comes from.

definition abbreviation theorem

legend

`BinderNameHint`

binderNameHint

The expression binderNameHint v binder e defined to be e.

If it is used on the right-hand side of an equation that is used for rewriting by rw or simp, and v is a local variable, and binder is an expression that (after beta-reduction) is a binder (fun w => … or ∀ w, …), then it will rename v to the name used in that binder, and remove the binderNameHint.

A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local variable is still name, and not x:

theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
    l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry

example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
  rw [all_eq_not_any_not]
  -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true

If binder is not a binder, then the name of v attains a macro scope. This only matters when the resulting term is used in a non-hygienic way, e.g. in termination proofs for well-founded recursion.

This gadget is supported by * simp, dsimp and rw in the right-hand-side of an equation * simp in the assumptions of congruence rules

It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics (e.g. apply).

def binderNameHint.{u, v, w} {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ

Used by: Component.Func.exists_settle

`Classical`

Exists.choose

Extract an element from an existential statement, using Classical.choose.

def Exists.choose.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : α

Used by: Component.Spec.toFunc, Discrete.size, Discrete.size_eq

Exists.choose_spec

Show that an element extracted from P : ∃ a, p a using P.choose satisfies p.

theorem Exists.choose_spec.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : p P.choose

Used by: Component.Spec.toFunc_spec, Discrete.size_eq

`Control.Id`

Id

The identity function on types, used primarily for its Monad instance.

The identity monad is useful together with monad transformers to construct monads for particular purposes. Additionally, it can be used with do-notation in order to use control structures such as local mutability, for-loops, and early returns in code that does not otherwise use monads.

Examples: lean example def containsFive (xs : List Nat) : Bool := Id.run do for x in xs do if x == 5 then return true return false

lean example #eval containsFive [1, 3, 5, 7]

true

def Id.{u} (type : Type u) : Type u

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

Id.run

Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type Id α, it causes do-notation in its arguments to use the Monad Id instance.

def Id.run.{u_1} {α : Type u_1} (x : Id α) : α

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

`Core`

Decidable.byContradiction

theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

Used by: Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, crc_detects_single_bit_flip, no_pow_two_eq_pow_three

Eq.mp

If h : α = β is a proof of type equality, then h.mp : α → β is the induced “cast” operation, mapping elements of α to elements of β.

You can prove theorems about the resulting element by induction on h, since rfl.mp is definitionally the identity function.

def Eq.mp.{u} {α β : Sort u} (h : α = β) (a : α) : β

Eq.mpr

If h : α = β is a proof of type equality, then h.mpr : β → α is the induced “cast” operation in the reverse direction, mapping elements of β to elements of α.

You can prove theorems about the resulting element by induction on h, since rfl.mpr is definitionally the identity function.

def Eq.mpr.{u} {α β : Sort u} (h : α = β) (b : β) : α

Exists

Existential quantification. If p : α → Prop is a predicate, then ∃ x : α, p x asserts that there is some x of type α such that p x holds. To create an existential proof, use the exists tactic, or the anonymous constructor notation ⟨x, h⟩. To unpack an existential, use cases h where h is a proof of ∃ x : α, p x, or let ⟨x, hx⟩ := h where `.

Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:

example (h : ∃ x : Nat, x = x) : Nat :=
  let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
  x

The error message recursor 'Exists.casesOn' can only eliminate into Prop means that this only works when the current goal is another proposition:

example (h : ∃ x : Nat, x = x) : True :=
  let ⟨x, _⟩ := h  -- ok, because the goal is `True : Prop`
  trivial

inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop

ForInStep

An indication of whether a loop’s body terminated early that’s used to compile the for x in xs notation.

A collection’s ForIn or ForIn' instance describes how to iterate over its elements. The monadic action that represents the body of the loop returns a ForInStep α, where α is the local state used to implement features such as let mut.

inductive ForInStep.{u} (α : Type u) : Type u

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

Iff

If and only if, or logical bi-implication. a ↔︎ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

Conventions for notations in identifiers:

The recommended spelling of ↔︎ in identifiers is iff.
The recommended spelling of <-> in identifiers is iff (prefer ↔︎ over <->).

structure Iff (a b : Prop) : Prop

Used by: BitSequence.trueCount_strict, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Receiver.step_correct

Nat.add_zero

theorem Nat.add_zero (n : ℕ) : n + 0 = n

Used by: Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Func.parallel_id_zero_right, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct, Component.Impl.parallel_empty, Component.Spec.monoidalCategory, Component.Spec.monoidalCategoryStruct, Component.Spec.parallel_id_zero_right, Component.Spec.trace_vanishing

Ne

a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

Conventions for notations in identifiers:

The recommended spelling of ≠ in identifiers is ne.

def Ne.{u} {α : Sort u} (a b : α) : Prop

Used by: BitSequence.trueCount_strict, Component.Func.exists_settle, InformationSystem.Run, InformationSystem.exists_repeat_state, InformationSystem.irreversible, InformationSystem.spontaneous_no_self_return, crc_detects_single_bit_flip, irrational_logb_two_three, no_pow_two_eq_pow_three

Ne.symm

theorem Ne.symm.{u} {α : Sort u} {a b : α} (h : a ≠ b) : b ≠ a

Used by: Component.Func.exists_settle

Not.intro

theorem Not.intro {a : Prop} (h : a → False) : ¬a

Quotient

Quotient types coarsen the propositional equality for a type so that terms related by some equivalence relation are considered equal. The equivalence relation is given by an instance of Setoid.

Set-theoretically, Quotient s can seen as the set of equivalence classes of α modulo the Setoid instance’s relation s.r. Functions from Quotient s must prove that they respect s.r: to define a function f : Quotient s → β, it is necessary to provide f' : α → β and prove that for all x : α and y : α, s.r x y → f' x = f' y. Quotient.lift implements this operation.

The key quotient operators are: * Quotient.mk places elements of the underlying type α into the quotient. * Quotient.lift allows the definition of functions from the quotient to some other type. * Quotient.sound asserts the equality of elements related by r * Quotient.ind is used to write proofs about quotients by assuming that all elements are constructed with Quotient.mk.

Quotient is built on top of the primitive quotient type Quot, which does not require a proof that the relation is an equivalence relation. Quotient should be used instead of Quot for relations that actually are equivalence relations.

def Quotient.{u} {α : Sort u} (s : Setoid α) : Sort u

Used by: Component.Impl.Hom, Component.Impl.Hom.recast_recast, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right

Quotient.ind

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk.

theorem Quotient.ind.{u} {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} :
  (∀ (a : α), motive ⟦a⟧) → ∀ (q : Quotient s), motive q

Quotient.liftOn

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient’s equivalence relation.

Given s : Setoid α and a quotient value q : Quotient s, applying a function f : α → β requires a proof c that f respects the equivalence relation s.r. In this case, the term Quotient.liftOn q f h : β reduces to the result of applying f to the underlying α value.

Quotient.lift is a version of this operation that takes the quotient value last, rather than first.

abbrev Quotient.liftOn.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β)
  (c : ∀ (a b : α), a ≈ b → f a = f b) : β

Used by: Component.Impl.Hom.toSpec

Quotient.mk

Places an element of a type into the quotient that equates terms according to an equivalence relation.

The setoid instance is provided explicitly. Quotient.mk' uses instance synthesis instead.

Given v : α, Quotient.mk s v : Quotient s is like v, except all observations of v’s value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

def Quotient.mk.{u} {α : Sort u} (s : Setoid α) (a : α) : Quotient s

Used by: Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.id, Component.Impl.Hom.recast_recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.tensorUnit, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.Hom.toSpec_comp

Quotient.sound

The quotient axiom, which asserts the equality of elements related in the setoid.

Because Quotient is built on a lower-level type Quot, Quotient.sound is implemented as a theorem. It is derived from Quot.sound, the soundness axiom for the lower-level quotient type Quot.

theorem Quotient.sound.{u} {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧

Used by: Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id_comp, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.monoidalCategory

Setoid

A setoid is a type with a distinguished equivalence relation, denoted ≈.

The Quotient type constructor requires a Setoid instance.

structure Setoid.{u} (α : Sort u) : Sort (max 1 u)

Used by: Component.Impl.Arrow.setoid

dif_neg

theorem dif_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :
  dite c t e = e hnc

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Fin.append_eval, Interface.tensor

dif_pos

theorem dif_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :
  dite c t e = t hc

funext

Function extensionality. If two functions return equal results for all possible arguments, then they are equal.

It is called “extensionality” because it provides a way to prove two objects equal based on the properties of the underlying mathematical functions, rather than based on the syntax used to denote them. Function extensionality is a theorem that can be proved using quotient types.

theorem funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = g

Used by: BitSequence.trueCount_strict, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.parallel_sequential, Component.Func.toSpec_injective, Component.Func.toSpec_sequential, Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_id, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.interchange, Component.Impl.monoidalCategory, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.symmetry_symmetry, Component.Spec.eq_toSpec_of_univalent, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.id_sequential, Component.Spec.parallel_assoc, Component.Spec.parallel_comm, Component.Spec.parallel_id_id, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.parallel_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.sequential_assoc, Component.Spec.sequential_id, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_superposing, Component.Spec.trace_vanishing, Component.Spec.trace_yanking

if_neg

theorem if_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (if c then t else e) = e

Used by: InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

if_pos

theorem if_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (if c then t else e) = t

Used by: InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

le_of_le_of_eq

theorem le_of_le_of_eq.{u_1} {α : Type u_1} {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c

noConfusionEnum

Auxiliary definition for generating compact noConfusion for enumeration types

abbrev noConfusionEnum.{u, v, w} {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w}
  {x y : α} (h : x = y) : noConfusionTypeEnum f P x y

Used by: Difficulty, TrafficLightColor

noConfusionTypeEnum

Auxiliary definition for generating compact noConfusion for enumeration types

abbrev noConfusionTypeEnum.{u, v, w} {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β)
  (P : Sort w) (x y : α) : Sort w

Used by: Difficulty, TrafficLightColor

`Data.Array.Basic`

Array.contains

Checks whether a is an element of as, using == to compare elements.

Array.elem is a synonym that takes the element before the array.

Examples: * #[1, 4, 2, 3, 3, 7].contains 3 = true * Array.contains #[1, 4, 2, 3, 3, 7] 5 = false

def Array.contains.{u} {α : Type u} [BEq α] (as : Array α) (a : α) : Bool

Used by: isExample, isIgnored, isLemma

`Data.Bool`

Bool.false_eq_true

These two rules follow trivially by simp, but are needed to avoid non-termination in false_eq and true_eq.

theorem Bool.false_eq_true : (false = true) = False

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

Bool.xor

Boolean “exclusive or”. xor x y can be written x ^^ y.

x ^^ y is true when precisely one of x or y is true. Unlike and and or, it does not have short-circuiting behavior, because one argument’s value never determines the final value. Also unlike and and or, there is no commonly-used corresponding propositional connective.

Examples: * false ^^ false = false * true ^^ false = true * false ^^ true = true * true ^^ true = false

Conventions for notations in identifiers:

The recommended spelling of ^^ in identifiers is xor.

abbrev Bool.xor : Bool → Bool → Bool

Used by: crc

`Data.Cast`

Nat.cast

The canonical homomorphism Nat → R. In most use cases, the target type will have a (semi)ring structure, and this homomorphism should be a (semi)ring homomorphism.

NatCast and IntCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a NatCast R instance) whenever R is an additive monoid with a 1.

The prototypical example is Int.ofNat.

def Nat.cast.{u} {R : Type u} [NatCast R] : ℕ → R

`Data.Fin.Basic`

Fin.cast

Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.

In other words, when eq : n = m, Fin.cast eq i converts i : Fin n into a Fin m.

def Fin.cast {n m : ℕ} (eq : n = m) (i : Fin n) : Fin m

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.recast, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Impl.parallel_empty, Component.Impl.recast, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.recast, Component.Spec.symmetry_symmetry, Component.Spec.trace_superposing, Component.Spec.trace_vanishing

Fin.castAdd

Coarsens a bound to one at least as large.

See also Fin.natAdd and Fin.addNat for addition functions that increase the bound, and Fin.castLE for a version that uses an explicit inequality proof.

def Fin.castAdd {n : ℕ} (m : ℕ) : Fin n → Fin (n + m)

Fin.castSucc

Coarsens a bound by one.

def Fin.castSucc {n : ℕ} : Fin n → Fin (n + 1)

Used by: LayeredArchitecture

Fin.elim0

The type Fin 0 is uninhabited, so it can be used to derive any result whatsoever.

This is similar to Empty.elim. It can be thought of as a compiler-checked assertion that a code path is unreachable, or a logical contradiction from which False and thus anything else could be derived.

def Fin.elim0.{u} {α : Sort u} : Fin 0 → α

Used by: Component.Func.discard, Component.Impl.empty, Component.Impl.empty_parallel, Component.Impl.monoidalCategory, Component.Impl.parallel_empty, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.trace_vanishing, Component.Spec.trace_yanking, Interface.unit, notRule_fixedPoint_unrealizable

Fin.natAdd

Adds a natural number to a Fin, increasing the bound.

This is a generalization of Fin.succ.

Fin.addNat is a version of this function that takes its Nat parameter second.

Examples: * Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11) * Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9) * Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)

def Fin.natAdd {m : ℕ} (n : ℕ) (i : Fin m) : Fin (n + m)

Fin.succ

The successor, with an increased bound.

This differs from adding 1, which instead wraps around.

Examples: * (2 : Fin 3).succ = (3 : Fin 4) * (2 : Fin 3) + 1 = (0 : Fin 3)

def Fin.succ {n : ℕ} : Fin n → Fin (n + 1)

Used by: LayeredArchitecture

Fin.val_congr

theorem Fin.val_congr {n : ℕ} {a b : Fin n} (h : a = b) : ↑a = ↑b

Used by: Fin.append_eval

`Data.Fin.Lemmas`

Fin.addCases

A case analysis operator for i : Fin (m + n) that separately handles the cases where i < m and where m ≤ i < m + n.

The first case, where i < m, is handled by left. In this case, i can be represented as Fin.castAdd n (j : Fin m).

The second case, where m ≤ i < m + n, is handled by right. In this case, i can be represented as Fin.natAdd m (j : Fin n).

def Fin.addCases.{u} {m n : ℕ} {motive : Fin (m + n) → Sort u}
  (left : (i : Fin m) → motive (Fin.castAdd n i)) (right : (i : Fin n) → motive (Fin.natAdd m i))
  (i : Fin (m + n)) : motive i

Used by: Component.Spec.parallel_id_id, Component.Spec.parallel_toSpec_eq

Fin.cast_refl

theorem Fin.cast_refl (n : ℕ) (h : n = n) : Fin.cast h = id

Used by: Component.Impl.parallel_empty, Component.Impl.recast, Component.Spec.symmetry_symmetry, Component.Spec.trace_vanishing

Fin.ext

theorem Fin.ext {n : ℕ} {a b : Fin n} (h : ↑a = ↑b) : a = b

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Fin.append_eval, InformationSystem.exists_repeat_state

Fin.natAdd_zero

theorem Fin.natAdd_zero {n : ℕ} : Fin.natAdd 0 = Fin.cast ⋯

Used by: Component.Spec.parallel_id_zero_left

`Data.Function`

Function.Injective

A function f : α → β is called injective if f x = f y implies x = y.

def Function.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Used by: Cell.erase_not_injective, Cell.erase_not_surjective, FiniteStateMachine.Reversible, InformationSystem.reversible

Function.Surjective

A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

def Function.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Used by: Cell.erase_not_surjective

`Data.Int.Basic`

Int

The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for Int that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually GMP). A “small number” is an integer that can be encoded with one fewer bits than the platform’s pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).

inductive Int : Type

Int.cast

The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

def Int.cast.{u} {R : Type u} [IntCast R] : ℤ → R

Used by: irrational_logb_two_three

Int.negOfNat

Negation of natural numbers.

Examples: * Int.negOfNat 6 = -6 * Int.negOfNat 0 = 0

def Int.negOfNat : ℕ → ℤ

Int.toNat

Converts an integer into a natural number. Negative numbers are converted to 0.

Examples: * (7 : Int).toNat = 7 * (0 : Int).toNat = 0 * (-7 : Int).toNat = 0

def Int.toNat : ℤ → ℕ

Used by: irrational_logb_two_three

`Data.Int.DivMod.Bootstrap`

Int.emod_def

theorem Int.emod_def (a b : ℤ) : a % b = a - b * (a / b)

Used by: no_pow_two_eq_pow_three

Int.lt_mul_ediv_self_add

theorem Int.lt_mul_ediv_self_add {x k : ℤ} (h : 0 < k) : x < k * (x / k) + k

Used by: no_pow_two_eq_pow_three

Int.mul_ediv_self_le

theorem Int.mul_ediv_self_le {x k : ℤ} (h : k ≠ 0) : k * (x / k) ≤ x

Used by: no_pow_two_eq_pow_three

Int.natCast_emod

theorem Int.natCast_emod (m n : ℕ) : ↑(m % n) = ↑m % ↑n

Used by: no_pow_two_eq_pow_three

`Data.Int.Lemmas`

Int.natCast_add

theorem Int.natCast_add (n m : ℕ) : ↑(n + m) = ↑n + ↑m

Int.natCast_mul

theorem Int.natCast_mul (n m : ℕ) : ↑(n * m) = ↑n * ↑m

Used by: no_pow_two_eq_pow_three

Int.sub_eq_zero_of_eq

theorem Int.sub_eq_zero_of_eq {a b : ℤ} (h : a = b) : a - b = 0

`Data.Int.Order`

Int.add_one_le_of_lt

theorem Int.add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b

Int.natCast_nonneg

theorem Int.natCast_nonneg (n : ℕ) : 0 ≤ ↑n

Int.sub_nonneg_of_le

theorem Int.sub_nonneg_of_le {a b : ℤ} (h : b ≤ a) : 0 ≤ a - b

Int.toNat_of_nonneg

theorem Int.toNat_of_nonneg {a : ℤ} (h : 0 ≤ a) : ↑a.toNat = a

Used by: irrational_logb_two_three

`Data.List.Basic`

List.Mem

List membership, typically accessed via the ∈ operator.

a ∈ l means that a is an element of the list l. Elements are compared according to Lean’s logical equality.

The related function List.elem is a Boolean membership test that uses a BEq α instance.

Examples: * a ∈ [x, y, z] ↔︎ a = x ∨ a = y ∨ a = z

inductive List.Mem.{u} {α : Type u} (a : α) : List α → Prop

Used by: Ontology.empty_wellFormed

List.any

Returns true if p returns true for any element of l.

O(|l|). Short-circuits upon encountering the first true.

Examples: * [2, 4, 6].any (· % 2 = 0) = true * [2, 4, 6].any (· % 2 = 1) = false * [2, 4, 5, 6].any (· % 2 = 0) = true * [2, 4, 5, 6].any (· % 2 = 1) = true

def List.any.{u} {α : Type u} (l : List α) (p : α → Bool) : Bool

Used by: crc_detects_single_bit_flip

List.filterMap

Applies a function that returns an Option to each element of a list, collecting the non-none values.

O(|l|).

Example: lean example #eval [1, 2, 5, 2, 7, 7].filterMap fun x => if x > 2 then some (2 * x) else none

[10, 14, 14]

def List.filterMap.{u, v} {α : Type u} {β : Type v} (f : α → Option β) : List α → List β

Used by: getConceptsOf

List.find?

Returns the first element of the list for which the predicate p returns true, or none if no such element is found.

O(|l|).

Examples: * [7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1 * [7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none

def List.find?.{u} {α : Type u} (p : α → Bool) : List α → Option α

Used by: resolveRelation

List.getLast

Returns the last element of a non-empty list.

Examples: * ["circle", "rectangle"].getLast (by decide) = "rectangle" * ["circle"].getLast (by decide) = "circle"

def List.getLast.{u} {α : Type u} (as : List α) : as ≠ [] → α

Used by: InformationSystem.Run.final

List.head

Returns the first element of a non-empty list.

def List.head.{u} {α : Type u} (as : List α) : as ≠ [] → α

Used by: InformationSystem.Run.initial

List.head?

Returns the first element in the list, if there is one. Returns none if the list is empty.

Use List.headD to provide a fallback value for empty lists, or List.head! to panic on empty lists.

Examples: * ([] : List Nat).head? = none * [3, 2, 1].head? = some 3

def List.head?.{u} {α : Type u} : List α → Option α

Used by: InformationSystem.Run.trajectory_head

List.headD

Returns the first element in the list if there is one, or fallback if the list is empty.

Use List.head? to return an Option, and List.head! to panic on empty lists.

Examples: * [].headD "empty" = "empty" * [].headD 2 = 2 * ["head", "shoulders", "knees"].headD "toes" = "head"

def List.headD.{u} {α : Type u} (as : List α) (fallback : α) : α

Used by: crc

List.replicate

Creates a list that contains n copies of a.

List.replicate 5 "five" = ["five", "five", "five", "five", "five"]
List.replicate 0 "zero" = []
List.replicate 2 ' ' = [' ', ' ']

def List.replicate.{u} {α : Type u} (n : ℕ) (a : α) : List α

Used by: crc

List.sum

Computes the sum of the elements of a list.

Examples: * [a, b, c].sum = a + (b + (c + 0)) * [1, 2, 5].sum = 8

def List.sum.{u_1} {α : Type u_1} [Add α] [Zero α] : List α → α

Used by: totalSize

List.tail

Drops the first element of a nonempty list, returning the tail. Returns [] when the argument is empty.

Examples: * ["apple", "banana", "grape"].tail = ["banana", "grape"] * ["apple"].tail = [] * ([] : List String).tail = []

def List.tail.{u} {α : Type u} : List α → List α

Used by: crc

List.take

Extracts the first n elements of xs, or the whole list if n is greater than xs.length.

O(min n |xs|).

Examples: * [a, b, c, d, e].take 0 = [] * [a, b, c, d, e].take 3 = [a, b, c] * [a, b, c, d, e].take 6 = [a, b, c, d, e]

def List.take.{u} {α : Type u} (n : ℕ) (xs : List α) : List α

Used by: InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state

List.zipWith

Applies a function to the corresponding elements of two lists, stopping at the end of the shorter list.

O(min |xs| |ys|).

Examples: * [1, 2].zipWith (· + ·) [5, 6] = [6, 8] * [1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13] * [].zipWith (· + ·) [5, 6] = [] * [x₁, x₂, x₃].zipWith f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

def List.zipWith.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α)
  (ys : List β) : List γ

Used by: crc

`Data.List.Control`

List.mapM

Applies the monadic action f to every element in the list, left-to-right, and returns the list of results.

This implementation is tail recursive. List.mapM' is a non-tail-recursive variant that may be more convenient to reason about. List.forM is the variant that discards the results and List.mapA is the variant that works with Applicative.

def List.mapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β)
  (as : List α) : m (List β)

Used by: Ontology.readFile

`Data.List.Lemmas`

List.eq_or_mem_of_mem_cons

theorem List.eq_or_mem_of_mem_cons.{u_1} {α : Type u_1} {a b : α} {l : List α} : a ∈ b :: l → a = b ∨ a ∈ l

Used by: InformationSystem.not_spontaneous_and_perpetuous

List.mem_append

theorem List.mem_append.{u_1} {α : Type u_1} {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Used by: InformationSystem.spontaneous_no_self_return

List.mem_cons_of_mem

theorem List.mem_cons_of_mem.{u_1} {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

Used by: InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

List.mem_cons_self

theorem List.mem_cons_self.{u_1} {α : Type u_1} {a : α} {l : List α} : a ∈ a :: l

Used by: InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

List.mem_singleton

theorem List.mem_singleton.{u_1} {α : Type u_1} {a b : α} : a ∈ [b] ↔ a = b

Used by: InformationSystem.spontaneous_no_self_return

`Data.List.OfFn`

List.ofFn

Creates a list by applying f to each potential index in order, starting at 0.

Examples: * List.ofFn (n := 3) toString = ["0", "1", "2"] * List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]

def List.ofFn.{u_1} {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α

Used by: Envelope.make, Envelope.valid, Receiver.step, Receiver.step_correct

`Data.Nat.Basic`

Nat.add_assoc

theorem Nat.add_assoc (n m k : ℕ) : n + m + k = n + (m + k)

Nat.add_lt_add_left

theorem Nat.add_lt_add_left {n m : ℕ} (h : n < m) (k : ℕ) : k + n < k + m

Used by: Component.Func.hexagon_reverse, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_reverse

Nat.eq_zero_or_pos

theorem Nat.eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0

Used by: no_pow_two_eq_pow_three

Nat.le_of_not_lt

theorem Nat.le_of_not_lt {a b : ℕ} : ¬a < b → b ≤ a

Nat.le_of_succ_le

theorem Nat.le_of_succ_le {n m : ℕ} (h : n.succ ≤ m) : n ≤ m

Used by: Component.Func.exists_settle

Nat.lt_add_right

theorem Nat.lt_add_right {a b : ℕ} (c : ℕ) (h : a < b) : a < b + c

Used by: Component.Func.hexagon_forward, Component.Impl.hexagon_forward_arrow, Component.Spec.hexagon_forward

Nat.lt_or_gt_of_ne

theorem Nat.lt_or_gt_of_ne {a b : ℕ} (ne : a ≠ b) : a < b ∨ a > b

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, no_pow_two_eq_pow_three

Nat.mul_assoc

theorem Nat.mul_assoc (n m k : ℕ) : n * m * k = n * (m * k)

Used by: card_BitFunction_succ_input

Nat.mul_comm

theorem Nat.mul_comm (n m : ℕ) : n * m = m * n

Used by: card_BitFunction

Nat.recAux

A recursor for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.rec. It is used by the induction tactic by default for Nat.

abbrev Nat.recAux.{u} {motive : ℕ → Sort u} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1))
  (t : ℕ) : motive t

Used by: Component.Func.exists_settle, Component.Func.iterate_dominates_succ

Nat.zero_add

theorem Nat.zero_add (n : ℕ) : 0 + n = n

Used by: Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Func.parallel_id_zero_left, Component.Impl.Hom.tensor_empty, Component.Impl.empty_parallel, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct, Component.Spec.monoidalCategory, Component.Spec.monoidalCategoryStruct, Component.Spec.parallel_id_zero_left

Nat.zero_lt_one

theorem Nat.zero_lt_one : 0 < 1

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

`Data.Nat.Lemmas`

Nat.le_self_pow

theorem Nat.le_self_pow {n : ℕ} (hn : n ≠ 0) (a : ℕ) : a ≤ a ^ n

Used by: no_pow_two_eq_pow_three

Nat.mod_succ

theorem Nat.mod_succ (n : ℕ) : n % n.succ = n

Used by: no_pow_two_eq_pow_three

Nat.pow_mod

theorem Nat.pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n

Used by: no_pow_two_eq_pow_three

`Data.Nat.Linear`

Nat.elimOffset

def Nat.elimOffset.{u} {α : Sort u} (a b k : ℕ) (h₁ : a + k = b + k) (h₂ : a = b → α) : α

Used by: NetworkBoundary

`Data.Range.Basic`

Std.Legacy.Range

structure Std.Legacy.Range : Type

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

`Data.Rat.Basic`

Rat

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

structure Rat : Type

Used by: irrational_logb_two_three

`Omega.Coeffs`

Lean.Omega.Coeffs.isZero

Are the coefficients all zero?

abbrev Lean.Omega.Coeffs.isZero (xs : Omega.Coeffs) : Prop

Used by: no_pow_two_eq_pow_three

Lean.Omega.Coeffs.ofList

Identity, turning List Int into Coeffs.

abbrev Lean.Omega.Coeffs.ofList (xs : List ℤ) : Omega.Coeffs

`Omega.Constraint`

Lean.Omega.Constraint.addEquality_sat

theorem Lean.Omega.Constraint.addEquality_sat {c : ℤ} {x y : Omega.Coeffs} (w : c + x.dot y = 0) :
  { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true

Lean.Omega.Constraint.addInequality_sat

theorem Lean.Omega.Constraint.addInequality_sat {c : ℤ} {x y : Omega.Coeffs} (w : c + x.dot y ≥ 0) :
  { lowerBound := some (-c), upperBound := none }.sat' x y = true

Lean.Omega.Constraint.combine_sat'

theorem Lean.Omega.Constraint.combine_sat' {s t : Omega.Constraint} {x y : Omega.Coeffs}
  (ws : s.sat' x y = true) (wt : t.sat' x y = true) : (s.combine t).sat' x y = true

Used by: Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, crc_detects_single_bit_flip, no_pow_two_eq_pow_three

Lean.Omega.Constraint.isImpossible

Check if a constraint is unsatisfiable.

def Lean.Omega.Constraint.isImpossible : Omega.Constraint → Bool

Lean.Omega.Constraint.not_sat'_of_isImpossible

theorem Lean.Omega.Constraint.not_sat'_of_isImpossible {c : Omega.Constraint} (h : c.isImpossible = true)
  {x y : Omega.Coeffs} : ¬c.sat' x y = true

Lean.Omega.combo_sat'

theorem Lean.Omega.combo_sat' (s t : Omega.Constraint) (a : ℤ) (x : Omega.Coeffs) (b : ℤ)
  (y v : Omega.Coeffs) (wx : s.sat' x v = true) (wy : t.sat' y v = true) :
  (Omega.Constraint.combo a s b t).sat' (Omega.Coeffs.combo a x b y) v = true

Used by: Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, no_pow_two_eq_pow_three

Lean.Omega.tidy_sat

theorem Lean.Omega.tidy_sat {s : Omega.Constraint} {x v : Omega.Coeffs} (w : s.sat' x v = true) :
  (Omega.tidyConstraint s x).sat' (Omega.tidyCoeffs s x) v = true

`Omega.Int`

Lean.Omega.Int.add_congr

theorem Lean.Omega.Int.add_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a + c = b + d

Lean.Omega.Int.mul_congr

theorem Lean.Omega.Int.mul_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a * c = b * d

Used by: no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_congr

theorem Lean.Omega.Int.ofNat_congr {a b : ℕ} (h : a = b) : ↑a = ↑b

Used by: Fin.append_eval, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_le_of_le

theorem Lean.Omega.Int.ofNat_le_of_le {x y : ℕ} (h : x ≤ y) : ↑x ≤ ↑y

Used by: Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Fin.append_eval, Interface.tensor, crc_detects_single_bit_flip, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_lt_of_lt

theorem Lean.Omega.Int.ofNat_lt_of_lt {x y : ℕ} (h : x < y) : ↑x < ↑y

Lean.Omega.Int.ofNat_pow

theorem Lean.Omega.Int.ofNat_pow (a b : ℕ) : ↑(a ^ b) = ↑a ^ b

Used by: no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_sub_dichotomy

theorem Lean.Omega.Int.ofNat_sub_dichotomy {a b : ℕ} : b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Lean.Omega.Int.ofNat_sub_sub

theorem Lean.Omega.Int.ofNat_sub_sub {a b c : ℕ} : ↑(a - b - c) = ↑(a - (b + c))

Lean.Omega.Int.sub_congr

theorem Lean.Omega.Int.sub_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a - c = b - d

`Omega.LinearCombo`

Lean.Omega.LinearCombo

Internal representation of a linear combination of atoms, and a constant term.

structure Lean.Omega.LinearCombo : Type

Lean.Omega.LinearCombo.add_eval

theorem Lean.Omega.LinearCombo.add_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs) :
  (l₁ + l₂).eval v = l₁.eval v + l₂.eval v

Lean.Omega.LinearCombo.coordinate

The i-th coordinate function.

def Lean.Omega.LinearCombo.coordinate (i : ℕ) : Omega.LinearCombo

Lean.Omega.LinearCombo.coordinate_eval_0

theorem Lean.Omega.LinearCombo.coordinate_eval_0 {a0 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 0).eval (Omega.Coeffs.ofList (a0 :: t)) = a0

Lean.Omega.LinearCombo.coordinate_eval_1

theorem Lean.Omega.LinearCombo.coordinate_eval_1 {a0 a1 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 1).eval (Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1

Lean.Omega.LinearCombo.coordinate_eval_2

theorem Lean.Omega.LinearCombo.coordinate_eval_2 {a0 a1 a2 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 2).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2

Lean.Omega.LinearCombo.coordinate_eval_3

theorem Lean.Omega.LinearCombo.coordinate_eval_3 {a0 a1 a2 a3 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 3).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

Used by: Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_4

theorem Lean.Omega.LinearCombo.coordinate_eval_4 {a0 a1 a2 a3 a4 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 4).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

Lean.Omega.LinearCombo.coordinate_eval_5

theorem Lean.Omega.LinearCombo.coordinate_eval_5 {a0 a1 a2 a3 a4 a5 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 5).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) =
    a5

Lean.Omega.LinearCombo.coordinate_eval_6

theorem Lean.Omega.LinearCombo.coordinate_eval_6 {a0 a1 a2 a3 a4 a5 a6 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 6).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) =
    a6

Used by: Component.Func.hexagon_reverse, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_reverse, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_7

theorem Lean.Omega.LinearCombo.coordinate_eval_7 {a0 a1 a2 a3 a4 a5 a6 a7 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 7).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) =
    a7

Used by: Component.Func.hexagon_reverse, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_reverse

Lean.Omega.LinearCombo.eval

Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩ at values [v_1, …, v_k] to obtain r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0)))).

def Lean.Omega.LinearCombo.eval (lc : Omega.LinearCombo) (values : Omega.Coeffs) : ℤ

Lean.Omega.LinearCombo.mul

Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.

def Lean.Omega.LinearCombo.mul (l₁ l₂ : Omega.LinearCombo) : Omega.LinearCombo

Used by: no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.mul_eval

theorem Lean.Omega.LinearCombo.mul_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs)
  (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) : (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Used by: no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.sub_eval

theorem Lean.Omega.LinearCombo.sub_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs) :
  (l₁ - l₂).eval v = l₁.eval v - l₂.eval v

`Prelude`

And

And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

Conventions for notations in identifiers:

The recommended spelling of ∧ in identifiers is and.

structure And (a b : Prop) : Prop

Array

Array α is the type of dynamic arrays with elements from α. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array, all updates will be performed destructively. This results in performance comparable to mutable arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while the capacity is the amount of memory currently allocated for elements. The size is accessible via Array.size, but the capacity is not observable from Lean code. Array.emptyWithCapacity n creates an array which is equal to #[], but internally allocates an array of capacity n. When the size exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, Array α is just a wrapper around List α.

structure Array.{u} (α : Type u) : Type u

Used by: Ontology.readFile, allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags, instDecodeTomlConcept, instDecodeTomlRawRelation, moduleOf

Array.size

Gets the number of elements stored in an array.

This is a cached value, so it is O(1) to access. The space allocated for an array, referred to as its capacity, is at least as large as its size, but may be larger. The capacity of an array is an internal detail that’s not observable by Lean code.

def Array.size.{u} {α : Type u} (a : Array α) : ℕ

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags, moduleOf

Bool

The Boolean values, true and false.

Logically speaking, this is equivalent to Prop (the type of propositions). The distinction is public important for programming: both propositions and their proofs are erased in the code generator, while Bool corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information.

inductive Bool : Type

Used by: Bit, BitSequence.Dominates.bot, BitSequence.trueCount_strict, Cell, Cell.erase_not_injective, Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Envelope, Envelope.make, Envelope.make_valid, Envelope.valid, Fin.append_eval, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Interface.tensor, Receiver.step, Receiver.step_correct, Sender.State, Sender.step, crc, crc_detects_single_bit_flip, discrete_Bool, eraseSecondBit, getConceptsOf, instDecidableEqCell, instFintypeCell, instNonemptyCell, instNonemptyEnvelope, instNonemptyState, instNormBool_computerNetworks, instNormEnvelope, instNormNonnegBit, instNormNonnegBool, instNormNonnegCell, instNormState, irrational_logb_two_three, isExample, isIgnored, isLemma, no_pow_two_eq_pow_three, notRule_fixedPoint_unrealizable, phone_number_information, three_doors_information, traffic_light_information

Bool.not

Boolean negation, also known as Boolean complement. not x can be written !x.

This is a function that maps the value true to false and the value false to true. The propositional connective is Not : Prop → Prop.

Conventions for notations in identifiers:

The recommended spelling of ! in identifiers is not.

def Bool.not : Bool → Bool

Used by: Bit.flip, Sender.step, crc_detects_single_bit_flip, notRule, notRule_fixedPoint_unrealizable

Decidable

Either a proof that p is true or a proof that p is false. This is equivalent to a Bool paired with a proof that the Bool is true if and only if p is true.

Decidable instances are primarily used via if-expressions and the tactic decide. In conditional expressions, the Decidable instance for the proposition is used to select a branch. At run time, this case distinction code is identical to that which would be generated for a Bool-based conditional. In proofs, the tactic decide synthesizes an instance of Decidable p, attempts to reduce it to isTrue h, and then succeeds with the proof h if it can.

Because Decidable carries data, when writing @[simp] lemmas which include a Decidable instance on the LHS, it is best to use {_ : Decidable p} rather than [Decidable p] so that non-canonical instances can be found via unification rather than instance synthesis.

inductive Decidable (p : Prop) : Type

Used by: InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Interface.tensor, Ontology.decidableWellFormed

Decidable.decide

Converts a decidable proposition into a Bool.

If p : Prop is decidable, then decide p : Bool is the Boolean value that is true if p is true and false if p is false.

def Decidable.decide (p : Prop) [h : Decidable p] : Bool

Used by: Cell.erase_not_injective, Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, Receiver.step, crc_detects_single_bit_flip, no_pow_two_eq_pow_three, notRule_fixedPoint_unrealizable, three_doors_information, traffic_light_information

DecidableEq

Propositional equality is Decidable for all elements of a type.

In other words, an instance of DecidableEq α is a means of deciding the proposition a = b is for all a b : α.

abbrev DecidableEq.{u} (α : Sort u) : Sort (max 1 u)

Used by: instDecidableEqCell

DecidablePred

A decidable predicate.

A predicate is decidable if the corresponding proposition is Decidable for each possible argument.

abbrev DecidablePred.{u} {α : Sort u} (r : α → Prop) : Sort (max 1 u)

Used by: BitSequence.trueCount_strict

EStateM.Result

The value returned from a combined state and exception monad in which exceptions do not automatically roll back the state.

Result ε σ α is equivalent to Except ε α × σ, but using a single combined inductive type yields a more efficient data representation.

inductive EStateM.Result.{u} (ε σ α : Type u) : Type u

Used by: Ontology.readFile

EStateM.run

Executes an EStateM action with the initial state s. The returned value includes the final state and indicates whether an exception was thrown or a value was returned.

def EStateM.run.{u} {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) : EStateM.Result ε σ α

Used by: Ontology.readFile

Eq

The equality relation. It has one introduction rule, Eq.refl. We use a = b as notation for Eq a b. A fundamental property of equality is that it is an equivalence relation.

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2. Example:

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t. For more information: Equality

Conventions for notations in identifiers:

The recommended spelling of = in identifiers is eq.

inductive Eq.{u_1} {α : Sort u_1} : α → α → Prop

Eq.ndrec_symm

Non-dependent recursor for the equality type (symmetric variant)

abbrev Eq.ndrec_symm.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α}
  (h : b = a) : motive b

Used by: Difficulty.ofString?

Eq.symm

Equality is symmetric: if a = b then b = a.

Because this is in the Eq namespace, if you have a variable h : a = b, h.symm can be used as shorthand for Eq.symm h as a proof of b = a.

For more information: Equality

theorem Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Eq.trans

Equality is transitive: if a = b and b = c then a = c.

Because this is in the Eq namespace, if you have variables or expressions h₁ : a = b and h₂ : b = c, you can use h₁.trans h₂ : a = c as shorthand for Eq.trans h₁ h₂.

For more information: Equality

theorem Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.exists_settle, Component.Func.fixedPoint_isFixed, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.iterate_stays, Component.Func.monoidalCategory, Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.parallel_sequential, Component.Func.recast_eqToHom, Component.Func.recast_recast, Component.Func.toImpl, Component.Func.toSpec_univalent, Component.Impl.Arrow.setoid, Component.Impl.Hom.recast_eqToHom, Component.Impl.Hom.recast_recast, Component.Impl.empty, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.id, Component.Impl.monoidalCategory, Component.Impl.parallel, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.parallel_empty, Component.Impl.recast, Component.Impl.recast_recast, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.monoidalCategory, Component.Spec.parallel_assoc, Component.Spec.parallel_comm, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_toSpec_eq, Component.Spec.recast_eqToHom, Component.Spec.recast_recast, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_vanishing, Component.Spec.trace_yanking, Fin.append_eval, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.sequential_delta, InformationSystem.spontaneous_no_self_return, Interface.tensor, card_BitSequence, crc_detects_single_bit_flip, eraseSecondBit, irrational_logb_two_three, no_pow_two_eq_pow_three, phone_number_information

Except

Except ε α is a type which represents either an error of type ε or a successful result with a value of type α.

Except ε : Type u → Type v is a Monad that represents computations that may throw exceptions: the pure operation is Except.ok and the bind operation returns the first encountered Except.error.

inductive Except.{u, v} (ε : Type u) (α : Type v) : Type (max u v)

Used by: Ontology.readFile, resolveRelation

False

False is the empty proposition. Thus, it has no introduction rules. It represents a contradiction. False elimination rule, False.rec, expresses the fact that anything follows from a contradiction. This rule is sometimes called ex falso (short for ex falso sequitur quodlibet), or the principle of explosion. For more information: Propositional Logic

inductive False : Prop

False.elim

False.elim : False → C says that from False, any desired proposition C holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.

The target type is actually C : Sort u which means it works for both propositions and types. When executed, this acts like an “unreachable” instruction: it is undefined behavior to run, but it will probably print “unreachable code”. (You would need to construct a proof of false to run it anyway, which you can only do using sorry or unsound axioms.)

def False.elim.{u} {C : Sort u} (h : False) : C

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.impossible_univalent, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous_no_self_return, NetworkBoundary, Ontology.empty_wellFormed

Fin

Natural numbers less than some upper bound.

In particular, a Fin n is a natural number i with the constraint that i < n. It is the canonical type with n elements.

structure Fin (n : ℕ) : Type

Function.comp

Function composition, usually written with the infix operator ∘. A new function is created from two existing functions, where one function’s output is used as input to the other.

Examples: * Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4] * (List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]

Conventions for notations in identifiers:

The recommended spelling of ∘ in identifiers is comp.

def Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ

GE.ge

a ≥ b is an abbreviation for b ≤ a.

Conventions for notations in identifiers:

The recommended spelling of ≥ in identifiers is ge.

def GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop

Used by: Fin.append_eval

GT.gt

a > b is an abbreviation for b < a.

Conventions for notations in identifiers:

The recommended spelling of > in identifiers is gt.

def GT.gt.{u} {α : Type u} [LT α] (a b : α) : Prop

Used by: Channel.lossy_loses_overall, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, no_pow_two_eq_pow_three

HEq

Heterogeneous equality. a ≍ b asserts that a and b have the same type, and casting a across the equality yields b, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as Eq, because the assumption that the types of a and b are equal is often too weak to prove theorems of interest. One public important non-theorem is the analogue of congr: If f ≍ g and x ≍ y and f x and g y are well typed it does not follow that f x ≍ g y. (This does follow if you have f = g instead.) However if a and b have the same type then a = b and a ≍ b are equivalent.

Conventions for notations in identifiers:

The recommended spelling of ≍ in identifiers is heq.

inductive HEq.{u} {α : Sort u} : α → {β : Sort u} → β → Prop

Used by: Channel, Component.Impl.Arrow, Envelope, FiniteStateMachine, InformationSystem, InformationSystem.Environment, InformationSystem.Run, InformationSystem.Step, InformationSystem.equivalent_output, InformationSystem.equivalent_step, Interface, LayeredArchitecture, NetworkBoundary, Ontology.empty_wellFormed, Sender.State

Lean.Name

Hierarchical names consist of a sequence of components, each of which is either a string or numeric, that are written separated by dots (.).

Hierarchical names are used to name declarations and for creating unique identifiers for free variables and metavariables.

You can create hierarchical names using a backtick:

`Lean.Meta.whnf

It is short for .str (.str (.str .anonymous "Lean") "Meta") "whnf".

You can use double backticks to request Lean to statically check whether the name corresponds to a Lean declaration in scope.

``Lean.Meta.whnf

If the name is not in scope, Lean will report an error.

There are two ways to convert a String to a Name:

Name.mkSimple creates a name with a single string component.
String.toName first splits the string into its dot-separated components, and then creates a hierarchical name.

inductive Lean.Name : Type

Used by: Channel.lossless_stationary, Channel.lossy_loses_overall, Envelope.make_valid, Receiver.step, Sender.step, allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags, crc_detects_single_bit_flip, getConceptsOf, isExample, isIgnored, isLemma, moduleOf

Lean.Name.mkStr1

Make name s₁

def Lean.Name.mkStr1 (s₁ : String) : Name

Used by: Ontology.readFile, concept, difficultyTag, exampleTag, ignoreTag, instDecodeTomlConcept, instDecodeTomlRawRelation, lemmaTag

Lean.ParserDescr

A ParserDescr is a grammar for parsers. This is used by the syntax command to produce parsers without having to import Lean.

inductive Lean.ParserDescr : Type

Used by: concept, difficultyTag, exampleTag, ignoreTag, lemmaTag

List

Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each element must be traversed to find the next element.

List α is isomorphic to Array α, but they are useful for different things: * List α is easier for reasoning, and Array α is modeled as a wrapper around List α. * List α works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared, Array α will have better performance because it can do destructive updates.

inductive List.{u} (α : Type u) : Type u

List.foldl

Folds a function over a list from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

Examples: * [a, b, c].foldl f z = f (f (f z a) b) c * [1, 2, 3].foldl (· ++ toString ·) "" = "123" * [1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"

def List.foldl.{u, v} {α : Type u} {β : Type v} (f : α → β → α) (init : α) : List β → α

Used by: crc

List.length

The length of a list.

This function is overridden in the compiler to lengthTR, which uses constant stack space.

Examples: * ([] : List String).length = 0 * ["green", "brown"].length = 2

def List.length.{u_1} {α : Type u_1} : List α → ℕ

Used by: Envelope.make, Envelope.valid, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, Receiver.step, Receiver.step_correct, Sender.State, Sender.step, crc, crc_detects_single_bit_flip, instNonemptyState, instNormState

List.map

Applies a function to each element of the list, returning the resulting list of values.

O(|l|).

Examples: * [a, b, c].map f = [f a, f b, f c] * [].map Nat.succ = [] * ["one", "two", "three"].map (·.length) = [3, 3, 5] * ["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]

def List.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List β

Used by: InformationSystem.Run.trajectory, totalSize

List.set

Replaces the value at (zero-based) index n in l with a. If the index is out of bounds, then the list is returned unmodified.

Examples: * ["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"] * ["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]

def List.set.{u_1} {α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α

Used by: crc_detects_single_bit_flip

List.toArray

Converts a List α into an Array α.

O(|xs|). At runtime, this operation is implemented by List.toArrayImpl and takes time linear in the length of the list. List.toArray should be used instead of Array.mk.

Examples: * [1, 2, 3].toArray = #[1, 2, 3] * ["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].

abbrev List.toArray.{u_1} {α : Type u_1} (xs : List α) : Array α

Used by: Ontology.readFile

Membership

The typeclass behind the notation a ∈ s : Prop where a : α, s : γ. Because α is an outParam, the “container type” γ determines the type of the elements of the container.

structure Membership.{u, v} (α : outParam (Type u)) (γ : Type v) : Type (max u v)

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allIgnoreTags, allLemmaTags

Nat

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually GMP); at runtime, Nat values that are sufficiently small are unboxed.

inductive Nat : Type

Nat.add

Addition of natural numbers, typically used via the + operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

def Nat.add : ℕ → ℕ → ℕ

Used by: NetworkBoundary

Nat.ble

The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples: * Nat.ble 2 5 = true * Nat.ble 5 2 = false * Nat.ble 5 5 = true

def Nat.ble : ℕ → ℕ → Bool

Used by: Difficulty, TrafficLightColor

Nat.le

Non-strict, or weak, inequality of natural numbers, usually accessed via the ≤ operator.

inductive Nat.le (n : ℕ) : ℕ → Prop

Used by: NetworkBoundary

Nat.le_succ_of_le

theorem Nat.le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ m.succ

Used by: Component.Func.iterate_settles

Nat.lt_of_not_le

theorem Nat.lt_of_not_le {a b : ℕ} (h : ¬a ≤ b) : b < a

Used by: Component.Func.exists_settle, InformationSystem.exists_repeat_state

Nat.lt_or_ge

theorem Nat.lt_or_ge (n m : ℕ) : n < m ∨ n ≥ m

Used by: Fin.append_eval

Nat.pow

The power operation on natural numbers, usually accessed via the ^ operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

def Nat.pow (m : ℕ) : ℕ → ℕ

Used by: phone_number_information

Nat.zero_le

theorem Nat.zero_le (n : ℕ) : 0 ≤ n

Used by: Component.Func.exists_settle

Nonempty

Nonempty α is a typeclass that says that α is not an empty type, that is, there exists an element in the type. It differs from Inhabited α in that Nonempty α is a Prop, which means that it does not actually carry an element of α, only a proof that there exists such an element. Given Nonempty α, you can construct an element of α nonconstructively using Classical.choice.

inductive Nonempty.{u} (α : Sort u) : Prop

Not

Not p, or ¬p, is the negation of p. It is defined to be p → False, so if your goal is ¬p you can use intro h to turn the goal into h : p ⊢ False, and if you have hn : ¬p and h : p then hn h : False and (hn h).elim will prove anything. For more information: Propositional Logic

Conventions for notations in identifiers:

The recommended spelling of ¬ in identifiers is not.

def Not (a : Prop) : Prop

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, Cell.erase_not_injective, Cell.erase_not_surjective, Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.not_cartesian, Component.Spec.parallel_assoc, Difficulty.ofString?, Fin.append_eval, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous, Interface.tensor, Ontology.readFile, crc_detects_single_bit_flip, irrational_logb_two_three, no_pow_two_eq_pow_three, notRule_fixedPoint_unrealizable, phone_number_information, three_doors_information

Option

Optional values, which are either some around a value from the underlying type or none.

Option can represent nullable types or computations that might fail. In the codomain of a function type, it can also represent partiality.

inductive Option.{u} (α : Type u) : Type u

Used by: Difficulty.ofString?, InformationSystem.Run.trajectory_head, getConceptsOf, moduleOf, resolveRelation

Option.getD

Gets an optional value, returning a given default on none.

This function is @[macro_inline], so dflt will not be evaluated unless opt turns out to be none.

Examples: * (some "hello").getD "goodbye" = "hello" * none.getD "goodbye" = "goodbye"

def Option.getD.{u_1} {α : Type u_1} (opt : Option α) (dflt : α) : α

Used by: Envelope.make, Envelope.valid, Receiver.step, Receiver.step_correct

Or

Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

Conventions for notations in identifiers:

The recommended spelling of ∨ in identifiers is or.

inductive Or (a b : Prop) : Prop

Used by: BitSequence.trueCount_strict, Fin.append_eval, InformationSystem.Step.delta_trichotomy, InformationSystem.eval_trichotomy, InformationSystem.exists_repeat_state, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous_no_self_return, no_pow_two_eq_pow_three

Or.elim

Proof by cases on an Or. If a ∨ b, and both a and b imply proposition c, then c is true.

theorem Or.elim {a b c : Prop} (h : a ∨ b) (left : a → c) (right : b → c) : c

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, Interface.tensor, no_pow_two_eq_pow_three

PProd

A product type in which the types may be propositions, usually written α ×' β.

This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.

Conventions for notations in identifiers:

The recommended spelling of ×' in identifiers is PProd.

structure PProd.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Used by: InformationSystem.eval

PULift

Lifts a type or proposition to a higher universe level.

PULift α wraps a value of type α. It is a generalization of PLift that allows lifting values whose type may live in Sort s. It also subsumes PLift.

structure PULift.{r, s} (α : Sort s) : Sort (max s r 1)

Used by: Difficulty, TrafficLightColor

PUnit

The canonical universe-polymorphic type with just one element.

It should be used in contexts that require a type to be universe polymorphic, thus disallowing Unit.

inductive PUnit.{u} : Sort u

Used by: InformationSystem.eval

Prod

The product type, usually written α × β. Product types are also called pair or tuple types. Elements of this type are pairs in which the first element is an α and the second element is a β.

Products nest to the right, so (x, y, z) : α × β × γ is equivalent to (x, (y, z)) : α × (β × γ).

Conventions for notations in identifiers:

The recommended spelling of × in identifiers is Prod.

structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

String

A string is a sequence of Unicode scalar values.

At runtime, strings are represented by dynamic arrays of bytes using the UTF-8 encoding. Both the size in bytes (String.utf8ByteSize) and in characters (String.length) are cached and take constant time. Many operations on strings perform in-place modifications when the reference to the string is unique.

structure String : Type

Used by: Concept, Difficulty.ofString?, Ontology.readFile, RawRelation, Relation, allConceptAnnotations, allDifficultyAnnotations, getConceptsOf, instDecodeTomlConcept, instDecodeTomlRawRelation, resolveRelation

String.Pos.Raw

A byte position in a String, according to its UTF-8 encoding.

Character positions (counting the Unicode code points rather than bytes) are represented by plain Nats. Indexing a String by a String.Pos.Raw takes constant time, while character positions need to be translated internally to byte positions, which takes linear time.

A byte position p is valid for a string s if 0 ≤ p ≤ s.rawEndPos and p lies on a UTF-8 character boundary, see String.Pos.IsValid.

There is another type, String.Pos, which bundles the validity predicate. Using String.Pos instead of String.Pos.Raw is recommended because it will lead to less error handling and fewer edge cases.

structure String.Pos.Raw : Type

Used by: Ontology.readFile

String.rawEndPos

A UTF-8 byte position that points at the end of a string, just after the last character.

"abc".rawEndPos = ⟨3⟩
"L∃∀N".rawEndPos = ⟨8⟩

def String.rawEndPos (s : String) : String.Pos.Raw

Used by: Ontology.readFile

True

True is a proposition and has only an introduction rule, True.intro : True. In other words, True is simply true, and has a canonical proof, True.intro For more information: Propositional Logic

inductive True : Prop

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.fixedPoint_isFixed, Component.Func.iterate_stays, Component.Func.monoidalCategory, Component.Func.parallel_sequential, Component.Impl.empty, Component.Impl.empty_parallel, Component.Impl.id, Component.Impl.monoidalCategory, Component.Impl.parallel, Component.Impl.parallel_comm, Component.Impl.parallel_empty, Component.Spec.monoidalCategory, Component.Spec.parallel_comm, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_toSpec_eq, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_yanking, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.sequential_delta, InformationSystem.spontaneous_no_self_return, card_BitSequence, eraseSecondBit, phone_number_information

Unit

The canonical type with one element. This element is written ().

Unit has a number of uses: * It can be used to model control flow that returns from a function call without providing other information. * Monadic actions that return Unit have side effects without computing values. * In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.

abbrev Unit : Type

Unit.unit

The only element of the unit type.

It can be written as an empty tuple: ().

abbrev Unit.unit : Unit

absurd

Anything follows from two contradictory hypotheses. Example:

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

For more information: Propositional Logic

def absurd.{v} {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b

Used by: BitSequence.Dominates.bot, Cell.erase_not_injective, InformationSystem.spontaneous_no_self_return

cast

Cast across a type equality. If h : α = β is an equality of types, and a : α, then a : β will usually not typecheck directly, but this function will allow you to work around this and embed a in type β as cast h a : β.

It is best to avoid this function if you can, because it is more complicated to reason about terms containing casts, but if the types don’t match up definitionally sometimes there isn’t anything better you can do.

For more information: Equality

def cast.{u} {α β : Sort u} (h : α = β) (a : α) : β

Used by: irrational_logb_two_three

cond

The conditional function.

cond c x y is the same as if c then x else y, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation bif c then x else y.

Just like ite, cond is declared @[macro_inline], which causes applications of cond to be unfolded. As a result, x and y are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated.

def cond.{u} {α : Sort u} (c : Bool) (x y : α) : α

Used by: Difficulty, TrafficLightColor

congr

Congruence in both function and argument. If f₁ = f₂ and a₁ = a₂ then f₁ a₁ = f₂ a₂. This only works for nondependent functions; the theorem statement is more complex in the dependent case.

For more information: Equality

theorem congr.{u, v} {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) :
  f₁ a₁ = f₂ a₂

Used by: BitSequence.trueCount_strict, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.monoidalCategory, Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.symmetry_symmetry, Component.Func.toImpl, Component.Impl.Hom.tensor_id_id, Component.Impl.empty, Component.Impl.empty_parallel, Component.Impl.equivalent_of_stationary, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.id, Component.Impl.id_sequential, Component.Impl.monoidalCategory, Component.Impl.parallel, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.parallel_empty, Component.Impl.recast, Component.Impl.sequential_assoc, Component.Impl.sequential_congr, Component.Impl.sequential_id, Component.Impl.symmetry, Component.Impl.symmetry_symmetry, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.monoidalCategory, Component.Spec.parallel_assoc, Component.Spec.parallel_comm, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_vanishing, Component.Spec.trace_yanking, InformationSystem.eval_delta, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, eraseSecondBit, irrational_logb_two_three, phone_number_information

congrArg

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

theorem congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

congrFun

Congruence in the function part of an application: If f = g then f a = g a.

theorem congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a

Used by: Component.Func.toSpec_injective, Component.Spec.parallel_id_id, Component.Spec.parallel_id_zero_left, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, notRule_fixedPoint_unrealizable

congrFun'

Similar to congrFun but β does not depend on α.

theorem congrFun'.{u, v} {α : Sort u} {β : Sort v} {f g : α → β} (h : f = g) (a : α) : f a = g a

Used by: BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.iterate_stays, Component.Func.monoidalCategory, Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Impl.Hom.tensor_id_id, Component.Impl.empty_parallel, Component.Impl.equivalent_of_stationary, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.id_sequential, Component.Impl.monoidalCategory, Component.Impl.parallel, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.parallel_empty, Component.Impl.sequential_assoc, Component.Impl.sequential_congr, Component.Impl.sequential_id, Component.Impl.symmetry_symmetry, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.monoidalCategory, Component.Spec.parallel_assoc, Component.Spec.parallel_comm, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.parallel_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, InformationSystem.eval_append, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, card_BitSequence, irrational_logb_two_three, no_pow_two_eq_pow_three, phone_number_information

dite

“Dependent” if-then-else, normally written via the notation if h : c then t(h) else e(h), is sugar for dite c (fun h => t(h)) (fun h => e(h)), and it is the same as if c then t else e except that t is allowed to depend on a proof h : c, and e can depend on h : ¬c. (Both branches use the same name for the hypothesis, even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches. For example, Array.get arr i h expects a proof h : i < arr.size in order to avoid a bounds check, so you can write if h : i < arr.size then arr.get i h else ... to avoid the bounds check inside the if branch. (Of course in this case we have only lifted the check into an explicit if, but we could also use this proof multiple times or derive i < arr.size from some other proposition that we are checking in the if.)

def dite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬c → α) : α

eq_of_heq

If two heterogeneously equal terms have the same type, then they are propositionally equal.

theorem eq_of_heq.{u} {α : Sort u} {a a' : α} (h : a ≍ a') : a = a'

id

The identity function. id takes an implicit argument α : Sort u (a type in any universe), and an argument a : α, and returns a.

Although this may look like a useless function, one application of the identity function is to explicitly put a type on an expression. If e has type T, and T' is definitionally equal to T, then @id T' e typechecks, and Lean knows that this expression has type T' rather than T. This can make a difference for typeclass inference, since T and T' may have different typeclass instances on them. show T' from e is sugar for an @id T' e expression.

def id.{u} {α : Sort u} (a : α) : α

inferInstance

inferInstance synthesizes a value of any target type by typeclass inference. This function has the same type signature as the identity function, but the square brackets on the [i : α] argument means that it will attempt to construct this argument by typeclass inference. (This will fail if α is not a class.) Example:

#check (inferInstance : Inhabited Nat) -- Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl

abbrev inferInstance.{u} {α : Sort u} [i : α] : α

ite

if c then t else e is notation for ite c t e, “if-then-else”, which decides to return t or e depending on whether c is true or false. The explicit argument c : Prop does not have any actual computational content, but there is an additional [Decidable c] argument synthesized by typeclass inference which actually determines how to evaluate c to true or false. Write if h : c then t else e instead for a “dependent if-then-else” dite, which allows t/e to use the fact that c is true/false.

def ite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α

Used by: InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, crc, getConceptsOf

liftM

Translates an action from monad m into monad n.

abbrev liftM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n]
  {α : Type u_1} : m α → n α

Used by: Ontology.readFile

noConfusion_of_Nat

A helper theorem to deduce False from a = b when f a ≠ f b for some function f : α → Nat (typically .ctorIdx). Used as a simpler alternative to the no-confusion theorems.

theorem noConfusion_of_Nat.{u} {α : Sort u} (f : α → ℕ) {a b : α} (h : a = b) :
  Bool.rec False True ((f a).beq (f b))

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, InformationSystem.not_spontaneous_and_perpetuous, NetworkBoundary, Ontology.empty_wellFormed

of_decide_eq_true

theorem of_decide_eq_true {p : Prop} [inst : Decidable p] : decide p = true → p

Used by: Cell.erase_not_injective, Component.Func.exists_settle, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_assoc, Fin.append_eval, InformationSystem.exists_repeat_state, Interface.tensor, crc_detects_single_bit_flip, no_pow_two_eq_pow_three, notRule_fixedPoint_unrealizable, three_doors_information, traffic_light_information

optParam

Gadget for optional parameter support.

A binder like (x : α := default) in a declaration is syntax sugar for x : optParam α default, and triggers the elaborator to attempt to use default to supply the argument if it is not supplied.

def optParam.{u} (α : Sort u) (default : α) : Sort u

Used by: Ontology.readFile

rfl

rfl : a = a is the unique constructor of the equality type. This is the same as Eq.refl except that it takes a implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although the statement of the theorem is a = a, Lean will allow anything that is definitionally equal to that type. So, for instance, 2 + 2 = 4 is proven in Lean by rfl, because both sides are the same up to definitional equality.

def rfl.{u} {α : Sort u} {a : α} : a = a

`PropLemmas`

decide_eq_true_iff

theorem decide_eq_true_iff {p : Prop} [Decidable p] : decide p = true ↔ p

Used by: Receiver.step_correct

`SimpLemmas`

Eq.mpr_not

theorem Eq.mpr_not {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p

Eq.mpr_prop

theorem Eq.mpr_prop {p q : Prop} (h₁ : p = q) (h₂ : q) : p

and_false

theorem and_false (p : Prop) : (p ∧ False) = False

Used by: InformationSystem.spontaneous_no_self_return

and_self

theorem and_self (p : Prop) : (p ∧ p) = p

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

dite_congr

theorem dite_congr.{u_1} {b c : Prop} {α : Sort u_1} {x✝ : Decidable b} [Decidable c] {x : b → α}
  {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c) (h₂ : ∀ (h : c), x ⋯ = u h)
  (h₃ : ∀ (h : ¬c), y ⋯ = v h) : dite b x y = dite c u v

eq_false'

theorem eq_false' {p : Prop} (h : p → False) : p = False

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, InformationSystem.not_spontaneous_and_perpetuous

eq_self

theorem eq_self.{u_1} {α : Sort u_1} (a : α) : (a = a) = True

Used by: BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.fixedPoint_isFixed, Component.Func.iterate_stays, Component.Func.monoidalCategory, Component.Func.parallel_sequential, Component.Impl.empty, Component.Impl.empty_parallel, Component.Impl.id, Component.Impl.monoidalCategory, Component.Impl.parallel, Component.Impl.parallel_comm, Component.Impl.parallel_empty, Component.Spec.monoidalCategory, Component.Spec.parallel_comm, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.parallel_toSpec_eq, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_yanking, Fin.append_eval, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.sequential_delta, card_BitSequence, eraseSecondBit, phone_number_information

eq_true

theorem eq_true {p : Prop} (h : p) : p = True

Used by: BitSequence.trueCount_strict, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

false_iff

theorem false_iff (p : Prop) : (False ↔ p) = ¬p

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

forall_congr

theorem forall_congr.{u} {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), p a = q a) :
  (∀ (a : α), p a) = ∀ (a : α), q a

Used by: Component.Func.exists_settle, InformationSystem.spontaneous_no_self_return

iff_false

theorem iff_false (p : Prop) : (p ↔ False) = ¬p

Used by: BitSequence.trueCount_strict

iff_self

theorem iff_self (p : Prop) : (p ↔ p) = True

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

iff_true

theorem iff_true (p : Prop) : (p ↔ True) = p

Used by: BitSequence.trueCount_strict

implies_congr

theorem implies_congr.{u, v} {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) :
  (p₁ → q₁) = (p₂ → q₂)

Used by: InformationSystem.spontaneous_no_self_return

implies_congr_ctx

theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

implies_true

theorem implies_true.{u} (α : Sort u) : (∀ (a : α), True) = True

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

not_false_eq_true

theorem not_false_eq_true : (¬False) = True

Used by: BitSequence.Dominates.bot, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous_no_self_return

not_true_eq_false

theorem not_true_eq_false : (¬True) = False

Used by: BitSequence.trueCount_strict

of_eq_true

theorem of_eq_true {p : Prop} (h : p = True) : p

or_false

theorem or_false (p : Prop) : (p ∨ False) = p

Used by: InformationSystem.spontaneous_no_self_return

true_and

theorem true_and (p : Prop) : (True ∧ p) = p

Used by: BitSequence.trueCount_strict

`SizeOf`

SizeOf

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a “size” function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

structure SizeOf.{u} (α : Sort u) : Sort (max 1 u)

Used by: Channel, Component.Impl.Arrow, FiniteStateMachine, InformationSystem, InformationSystem.Environment, InformationSystem.Run, InformationSystem.Step, LayeredArchitecture

`System.FilePath`

System.FilePath

A path on the file system.

Paths consist of a sequence of directories followed by the name of a file or directory. They are delimited by a platform-dependent separator character (see System.FilePath.pathSeparator).

structure System.FilePath : Type

Used by: Ontology.readFile

`System.IO`

BaseIO

An IO monad that cannot throw exceptions.

def BaseIO (α : Type) : Type

Used by: Ontology.readFile

EIO

A monad that can have side effects on the external world or throw exceptions of type ε.

BaseIO is a version of this monad that cannot throw exceptions. IO sets the exception type to IO.Error.

def EIO (ε α : Type) : Type

Used by: Ontology.readFile

EIO.toBaseIO

Converts an EIO ε action that might throw an exception of type ε into an exception-free BaseIO action that returns an Except value.

def EIO.toBaseIO {ε α : Type} (act : EIO ε α) : BaseIO (Except ε α)

Used by: Ontology.readFile

IO

A monad that supports arbitrary side effects and throwing exceptions of type IO.Error.

abbrev IO : Type → Type

Used by: Ontology.readFile

IO.FS.readFile

Reads the entire contents of the UTF-8-encoded file at the given path as a String.

An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to exceptions that may always be thrown as a result of failing to read files.

def IO.FS.readFile (fname : System.FilePath) : IO String

Used by: Ontology.readFile

`System.IOError`

IO.Error

Exceptions that may be thrown in the IO monad.

Many of the constructors of IO.Error correspond to POSIX error numbers. In these cases, the documentation string lists POSIX standard error macros that correspond to the error. This list is not necessarily exhaustive, and these constructor includes a field for the underlying error number.

inductive IO.Error : Type

Used by: Ontology.readFile

IO.userError

Constructs an IO.Error from a string.

IO.Error is the type of exceptions thrown by the IO monad.

def IO.userError (s : String) : IO.Error

Used by: Ontology.readFile