Skip to content
GitLab
Commit 9206b460 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Minor clean up

parent 7c2021bd
Hide whitespace changes
Inline Side-by-side
theories/logrel.v
View file @ 9206b460
......@@ -131,12 +131,6 @@ Section logrel.
iFrame.
Qed.
(* Definition to_side (s : side) : chan:= *)
(* match s with *)
(* | Left => true *)
(* | Right => false *)
(* end. *)
Coercion side_to_side (s : side) : channel.side :=
match s with Left => channel.Left | Right => channel.Right end.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment