module Stdlib.Trait.Ord; open import Stdlib.Data.Bool.Base; type Ordering := | LT : Ordering | EQ : Ordering | GT : Ordering; isLT : Ordering → Bool; isLT LT := true; isLT _ := false; isEQ : Ordering → Bool; isEQ EQ := true; isEQ _ := false; isGT : Ordering → Bool; isGT GT := true; isGT _ := false; --- A trait for defining a total order type Ord (A : Type) := | mkOrd : (A -> A -> Ordering) -> Ord A;Last modified on 2023-05-08 11:40 UTC