Fix assign-call

francescoo22 · Aug 22, 2024 · 4448420 · 4448420
1 parent 86c997c
commit 4448420
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/annotation-system/rules/statements.typ b/src/annotation-system/rules/statements.typ
@@ -101,8 +101,9 @@
   axiom($Delta(p) = alpha' beta'$),
   axiom($Delta tr m(overline(p)) tl Delta_1$),
   axiom($mtype(m) = alpha_0 beta_0, ..., alpha_n beta_n -> alpha$),
+  axiom($(beta' = borrowed) => (alpha = unique)$),
   axiom($Delta_1[p |-> alpha] = Delta'$),
-  rule(n:4, label: "Assign-Call", $mid(p = m(overline(p)))'$)
+  rule(n:5, label: "Assign-Call", $mid(p = m(overline(p)))'$)
 )
 
 #let Call = {