Lvc.Constr.CSetComputable

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Export SetDecide.

Require Import EqDec CSetNotation.

Global Instance inst_eq_dec_ordered_type X `(OrderedType X)
  : @EqDec X _ OT_Equivalence.
Defined.

Instance inst_computable_In X `(OrderedType X) x s
  : Computable(x ∈ s).
Defined.

Instance Subset_computable {X} `{OrderedType X} {s t:set X}
  : Computable (Subset s t).

Instance Equal_computable X `{OrderedType X} (s t:set X) : Computable (s [=] t).
Defined.

Instance equiv_computable X `{OrderedType X} (x y: X) : Computable (_eq x y).
Defined.

Extraction Inline inst_computable_In Subset_computable Equal_computable.