Require Export tactics2.
Require Export EquivDec.


Section Node.

  (* Type with decidable equality *)
  Class Node :=
    MkNode {
        (* The internal nodes for which we're going to assign state machines *)
        name : Set;
        (* The external nodes, to which we can send messages but that are not running our state machines *)
        (*    ename : Type;*)

        (* both these types have to have decidable equality *)
        name_dec : Deq name;
        (*    external_name_dec : Deq ename;*)
      }.

  (* example of Node where both internal and external nodes are modeled as natural numbers *)
  Instance nat_node : Node := MkNode nat eq_nat_dec.

End Node.
