8000 Merge `improvement/sync-channel-definition` of pull request #119 into… · input-output-hk/thorn-calculus@750a483 · GitHub
[go: up one dir, main page]
Skip to content

Commit 750a483

Browse files
jeltschjeltsch
committed
Merge improvement/sync-channel-definition of pull request #119 into master
Improve the definition of `sync_channel`
2 parents 3f1727d + 59c26da commit 750a483

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