details

examples/lambda-mu.bitts

@@ -1,5 +1,5 @@
-(* A variant of the λμ-caculus *)
 
+(* A variant of the λμ-caculus *)
 
 sort Ty ()
 sort Tm (A : Ty)
@@ -14,14 +14,14 @@ sort Addr (A : Ty)
 constructor ⊥ () (): Ty
 
 constructor μ (A : Ty) (t{x : Addr(A)} : Tm(⊥)) : Tm(A)
-constructor concat (A : Ty, B : Ty) (a : Addr(B), t : Tm(A)) : Addr(→(A, B))
+constructor ◁ (A : Ty, B : Ty) (a : Addr(B), t : Tm(A)) : Addr(→(A, B))
 destructor send (A : Ty) [a : Addr(A)] (t : Tm(A)) : Tm(⊥)
 
 equation skipcheck
-    send(concat(a, u), t) --> send(a, ﹫(t, u))
+    send(◁(a, u), t) --> send(a, ﹫(t, u))
 
 equation skipcheck
-    ﹫(μ(a. t{a}), u) --> μ(a. t{concat(a, u)})
+    ﹫(μ(a. t{a}), u) --> μ(a. t{◁(a, u)})
 
 let pierce (P : Ty, Q : Ty) : Tm(→(→(→(P, Q), P), P))
     := λ(f. μ(a. send(a, ﹫(f, λ(p. μ(_. send(a, p)))))))