Library Atom
Atoms are structureless objects such that we can always generate
one fresh from a finite collection. Equality on atoms is eq and
decidable. We use Coq's module system to make abstract the
implementation of atoms. The module type ATOM, defined below,
is compatible with UsualDecidableType.
Module Type ATOM.
Parameter t : Set.
Definition eq := @eq t.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Parameter eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
Parameter atom_fresh_for_list :
∀ (xs : list t), {x : t | ~ List.In x xs}.
End ATOM.
The implementation of the above interface is hidden for
documentation purposes.
We give more suggestive names to some of the constants provided by
the AtomImpl module.
Definition atom : Set :=
AtomImpl.t.
Definition eq_atom_dec : ∀ (x y : atom), {x = y} + {x ≠ y} :=
AtomImpl.eq_dec.
Hint Resolve eq_atom_dec.
This page has been generated by coqdoc