8000 Improve the definition of `sync_channel` · input-output-hk/thorn-calculus@59c26da · GitHub
[go: up one dir, main page]
Skip to content

Commit 59c26da

Browse files
jeltschjeltsch
committed
Improve the definition of sync_channel 
1 parent 3f1727d commit 59c26da

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

‎src/Thorn_Calculus-Derived-Channels-Synchronous.thy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ theory "Thorn_Calculus-Derived-Channels-Synchronous"
1111
begin
1212

1313
typedef 'a sync_channel = "UNIV :: 'a channel channel set"
14-
using UNIV_witness .
14+
morphisms sync_channel_to_nested_channel sync_channel_from_nested_channel ..
1515

1616
lift_definition
1717
sync_send :: "'a sync_channel \<Rightarrow> 'a \<Rightarrow> process \<Rightarrow> process"

0 commit comments

Comments
 (0)
0