Message
Let us define the notion of message. As simple as the following:
Definition interface_id := ident.
Definition content := Type.
Inductive message : Type :=
| Message : ident -> binding -> content -> message.
In the above definition of message, with defined
the content part of the message of being of type
Type. As such, we need to use the following axiom
in order to be able to have decidabilty over
messages. Nothing scary...
Axiom message_dec:
forall (m m' : (message)), {m = m'} + {m <> m'}.
Hint Resolve message_dec.
Function beq_message (m1 m2: message) : bool :=
match m1, m2 with
Message id1 b1 x, Message id2 b2 x' => (id1 == id2) && (b1 == b2)%bind
end.
Bind Scope message_scope with message.
Delimit Scope message_scope with msg.
Notation "m1 '==' m2" := (beq_message m1 m2) (at level 80) : message_scope.
Function get_message_path (m:message) : path :=
match m with
| Message id b x => (b->path)%bind
end.
Notation "m '->path'" := (get_message_path m) (at level 80) : message_scope.