From PslBase Require Import FinTypes.

Plain undirected graphs


Record UGraph :=
  {
    V : finType;
    E : V * V -> Prop;
    E_dec : forall v1 v2, {E (v1, v2)} + {~ E (v1, v2)};
    E_symm: forall v1 v2, E (v1, v2) <-> E (v2, v1)
  }.