Library Atom
Require Import Arith.
Require Import DecidableTypeEx.
Require Import List.
Require Import Max.
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 : forall x y : t, {x = y} + {x <> y}.
Parameter atom_fresh_for_list :
forall (xs : list t), {x : t | ~ List.In x xs}.
End ATOM.
The implementation of the above interface is hidden for
documentation purposes.
Module AtomImpl : ATOM.
End AtomImpl.
We give more suggestive names to some of the constants provided by
the
AtomImpl
module.
Definition atom := AtomImpl.t.
Definition eq_atom_dec := AtomImpl.eq_dec.
This page has been generated by coqdoc