blob: 31e9ce8057917dfb4e166f71ab434269f9339023 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import FSets.
Require Import InterfGraphMapImp.
Record irc_graph := Make_IRC_Graph {
irc_g : tt;
irc_wl : WS;
pal : VertexSet.t;
irc_k : nat;
HWS_irc : WS_properties irc_g irc_k irc_wl;
Hk : VertexSet.cardinal pal = irc_k
}.
Definition graph_to_IRC_graph g palette :=
let K := VertexSet.cardinal palette in
Make_IRC_Graph g (get_WL g K) palette K (WS_prop_get _ _) (refl_equal _).
|
