0725349bbd
This PR introduces a canonical way to endow a type with an order structure. The basic operations (`LE`, `LT`, `Min`, `Max`, and in later PRs `BEq`, `Ord`, ...) and any higher-level property (a preorder, a partial order, a linear order etc.) are then put in relation to `LE` as necessary. The PR provides `IsLinearOrder` instances for many core types and updates the signatures of some lemmas. **BREAKING CHANGES:** * The requirements of the `lt_of_le_of_lt`/`le_trans` lemmas for `Vector`, `List` and `Array` are simplified. They now require an `IsLinearOrder` instance. The new requirements are logically equivalent to the old ones, but the `IsLinearOrder` instance is not automatically inferred from the smaller typeclasses. * Hypotheses of type `Std.Total (¬ · < · : α → α → Prop)` are replaced with the equivalent class `Std.Asymm (· < · : α → α → Prop)`. Breakage should be limited because there is now an instance that derives the latter from the former. * In `Init.Data.List.MinMax`, multiple theorem signatures are modified, replacing explicit parameters for antisymmetry, totality, `min_ex_or` etc. with corresponding instance parameters.
13 lines
302 B
Text
13 lines
302 B
Text
/-
|
|
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
module
|
|
|
|
prelude
|
|
public import Init.Data.Char.Basic
|
|
public import Init.Data.Char.Lemmas
|
|
public import Init.Data.Char.Order
|
|
|
|
public section
|