Skip to content

Commit d70bfdc

Browse files
committed
mend
feat: implement links notation and added imports
1 parent 17768e4 commit d70bfdc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

CoqOfRust/links/M.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -345,7 +345,7 @@ Definition output_with_exception (Output : Set) `{Link Output} (output : Output
345345
match output with
346346
| inl output => inl (φ output)
347347
| inr exception => inr exception
348-
end.u
348+
end.
349349

350350
Module Run.
351351
Reserved Notation "{{ e ⇓ output_to_value }}" (no associativity).

0 commit comments

Comments
 (0)