Qcert.Basic.Data.RDataSort

Section SortableData.
  Inductive SortDesc : Set := | Descending | Ascending.
  Definition SortCriteria : Set := string × SortDesc.
  Definition SortCriterias : Set := list SortCriteria.


  Inductive sdata :=
  | sdnat : Z → sdata
  | sdstring : string → sdata
  .

  Lemma sort_desc_eq_dec : ∀ x y:SortDesc, {x=y}+{x≠y}.

  Lemma sdata_eq_dec : ∀ x y:sdata, {x=y}+{x≠y}.