rainbow.math.nat.linear-order

logic/decidable-relation

DefinitionSource, line 55

logic/decidable-relation.{u} :
  (A : Type u) (relation : A → A → Prop)
  → Type u

logic/decidable-equality

DefinitionSource, line 69

logic/decidable-equality.{u} :
  (A : Sort u)
  → Sort [:imax [:param u] [:max [:succ [:zero]] [:param u]]]

logic/if-data

DefinitionSource, line 79

logic/if-data.{u} :
  (A : Sort u) (condition : Prop) (decision : data/Bool) (x₁ x₂ : A)
  → A

order/min-operation

DefinitionSource, line 97

order/min-operation.{u} :
  (A : Type u) (dictionary : A → A → A) (x₁ x₂ : A)
  → A

order/max-operation

DefinitionSource, line 111

order/max-operation.{u} :
  (A : Type u) (dictionary : A → A → A) (x₁ x₂ : A)
  → A

order/le-class

DefinitionSource, line 119

order/le-class.{u} :
  (A : Type u) (relation : A → A → Prop) (x₁ x₂ : A)
  → Prop

order/lt-class

DefinitionSource, line 133

order/lt-class.{u} :
  (A : Type u) (relation : A → A → Prop) (x₁ x₂ : A)
  → Prop

nat/decide-at-most

DefinitionSource, line 141

nat/decide-at-most :
  (x₁ x₂ : ℕ)
  → data/Bool

ℕ = data/Nat

nat/decide-strict-below

DefinitionSource, line 169

nat/decide-strict-below :
  (x₁ x₂ : ℕ)
  → data/Bool

ℕ = data/Nat

nat/decide-equality

DefinitionSource, line 180

nat/decide-equality :
  (x₁ x₂ : ℕ)
  → data/Bool

ℕ = data/Nat

nat/min

DefinitionSource, line 215

nat/min :
  (x₁ x₂ : ℕ)
  → ℕ

ℕ = data/Nat

nat/max

DefinitionSource, line 228

nat/max :
  (x₁ x₂ : ℕ)
  → ℕ

ℕ = data/Nat

order/compare-operation

DefinitionSource, line 241

order/compare-operation.{u} :
  (A : Type u) (dictionary : A → A → order/Ordering) (x₁ x₂ : A)
  → order/Ordering

order/compare-from-less-equal

DefinitionSource, line 259

order/compare-from-less-equal.{u} :
  (A : Type u) (left right : A) (less-than : A → A → Prop) (less-decision : data/Bool)
  (equality-decision : A → A → data/Bool)
  → order/Ordering

nat/ordering

DefinitionSource, line 291

nat/ordering :
  (x₁ x₂ : ℕ)
  → order/Ordering

ℕ = data/Nat