From ade99f3f1fc2da1d51a82f1376c61ad609d60ff1 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Tue, 12 Dec 2023 17:58:46 +0530
Subject: feat: associativity and commutativity for addition

---
 src/nat.ts | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

(limited to 'src/nat.ts')

diff --git a/src/nat.ts b/src/nat.ts
index 86bd318..124c2c6 100644
--- a/src/nat.ts
+++ b/src/nat.ts
@@ -1,16 +1,9 @@
-declare const prev: unique symbol
+import { Op } from "./util";
 
-export type _nat = number & { [prev]: _nat | null }
-export type Succ<n extends _nat> = number & { [prev]: n }
-export type Pred<n extends _nat> = n extends _0 ? n : n[typeof prev]
-export type Nat = _0 | Succ<_nat>
+export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B };
+export type Succ<A extends Op> = Add<'1', A>;
 
-export type _0 = 0 & { [prev]: null }
+export type _0 = '0'
 export type _1 = Succ<_0>
 export type _2 = Succ<_1>
 export type _3 = Succ<_2>
-export type _4 = Succ<_3>
-export type _5 = Succ<_4>
-export type _6 = Succ<_5>
-export type _7 = Succ<_6>
-export type _8 = Succ<_7>
-- 
cgit v1.3.1