Cedar.Data.LT

This file contains utilities for working with strict and decidable LT relations.

source

class Cedar.Data.StrictLT (α : Type u_1) [LT α] :

Prop

asymmetric (a b : α) : a < b → ¬b < a
transitive (a b c : α) : a < b → b < c → a < c
connected (a b : α) : a ≠ b → a < b ∨ b < a

Instances

source

theorem Cedar.Data.StrictLT.irreflexive {α : Type u_1} [LT α] [StrictLT α] (x : α) :

¬x < x

source

theorem Cedar.Data.StrictLT.if_not_lt_gt_then_eq {α : Type u_1} [LT α] [StrictLT α] (x y : α) :

¬x < y → ¬y < x → x = y

source

theorem Cedar.Data.StrictLT.if_not_lt_eq_then_gt {α : Type u_1} [LT α] [StrictLT α] (x y : α) :

¬x < y → ¬x = y → x > y

source

theorem Cedar.Data.StrictLT.not_eq {α : Type u_1} [LT α] [StrictLT α] (x y : α) :

x < y → ¬x = y

source

theorem List.cons_lt_cons {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] (x : α) (xs ys : List α) :

xs < ys → x :: xs < x :: ys

source

theorem List.slt_irrefl {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs : List α) :

¬xs < xs

source

theorem List.slt_trans {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] {xs ys zs : List α} :

xs < ys → ys < zs → xs < zs

source

theorem List.slt_asymm {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {xs ys : List α} :

xs < ys → ¬ys < xs

source

theorem List.lt_conn {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] {xs ys : List α} :

xs ≠ ys → xs < ys ∨ ys < xs

source

instance List.strictLT (α : Type u_1) [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] :

Cedar.Data.StrictLT (List α)

source

def Bool.lt (a b : Bool) :

Bool

Equations

false.lt true = true
a.lt b = false

Instances For

source

instance instLTBool_cedar :

LT Bool

Equations

instLTBool_cedar = { lt := fun (a b : Bool) => a.lt b = true }

source

instance Bool.decLt (a b : Bool) :

Decidable (a < b)

Equations

a.decLt b = if h : a.lt b = true then isTrue h else isFalse h

source

instance Bool.strictLT :

Cedar.Data.StrictLT Bool

source

instance Nat.strictLT :

Cedar.Data.StrictLT Nat

source

instance Int.strictLT :

Cedar.Data.StrictLT Int

source

instance UInt32.strictLT :

Cedar.Data.StrictLT UInt32

source

instance Char.strictLT :

Cedar.Data.StrictLT Char

source

instance String.strictLT :

Cedar.Data.StrictLT String