Tealeaves.LN.Atom

From Tealeaves Require Import
     Util.Prelude Util.EqDec_eq
     Singlesorted.Functors.List.

Import SetlikeFunctor.Notations.
#[local] Open Scope tealeaves_scope.

This type has been borrowed from Metalib and lightly adapted for Tealeaves. https://github.com/plclub/metalib/blob/master/Metalib/MetatheoryAtom.v
Module Type ATOM <: UsualDecidableType.

  Parameter atom : Set.

  Definition t := atom.

  Parameter eq_dec : forall x y : atom, {x = y} + {x <> y}.

  Parameter atom_fresh_for_list :
    forall (xs : list t), {x : atom | ~ x xs}.

  Parameter fresh : list atom -> atom.

  Parameter fresh_not_in : forall l, ~ fresh l l.

  Parameter nat_of : atom -> nat.

  #[export] Hint Resolve eq_dec : core.

  Include HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.

End ATOM.

The implementation of the above interface is hidden for documentation purposes.
Module Atom : ATOM.


End Atom.

Notation atom := Atom.atom.
Notation fresh := Atom.fresh.
Notation fresh_not_in := Atom.fresh_not_in.
Notation atom_fresh_for_list := Atom.atom_fresh_for_list.

(* Automatically unfold Atom.eq *)
Global Arguments Atom.eq /.

It is trivial to declare an instance of EqDec for atom.
Instance EqDec_atom : @EqDec atom eq eq_equivalence.
Proof.
  exact Atom.eq_dec.
Defined.