Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- record Ord (A : Set) : Set₁ where
- field
- _≤_ _>_ : A → A → Set
- _≤≤_ : {a₀ a₁ a₂ : A} → a₀ ≤ a₁ → a₁ ≤ a₂ → a₀ ≤ a₂
- _>>_ : {a₀ a₁ a₂ : A} → a₀ > a₁ → a₁ > a₂ → a₀ > a₂
- _∀≤∨>_ : (a₀ a₁ : A) → a₀ ≤ a₁ ∨ a₀ > a₁
- _∄≤∧>_ : {a₀ a₁ : A} → a₀ ≤ a₁ → a₀ > a₁ → ⊥
- ≤zero : {a : A} → a ≤ a
Advertisement
