From 52f44422879de15527081c0c58e16bbcf03830f6 Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Fri, 19 Apr 2024 10:16:32 +0200 Subject: [PATCH] details --- examples/lambda-mu.bitts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/lambda-mu.bitts b/examples/lambda-mu.bitts index 50e4c64..e4a4699 100644 --- a/examples/lambda-mu.bitts +++ b/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)))))))