Module Qcert.Utils.SortingDesc

Require Import Orders.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import String.
Require Import List.
Require Import StringAdd.

Section SortingDesc.
  Inductive SortDesc : Set := | Descending | Ascending.
  Definition SortCriteria : Set := string * SortDesc.
  Definition SortCriterias : Set := list SortCriteria.

  Lemma sort_desc_eq_dec : forall x y:SortDesc, {x=y}+{x<>y}.
  
  Global Instance sort_desc_eqdec : EqDec SortDesc eq := sort_desc_eq_dec.

End SortingDesc.