diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-10 16:15:00 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-10 16:32:23 +0530 |
| commit | f6e26212620de411e082cbd52379075ea5a99032 (patch) | |
| tree | a7a68c681a3e99987f2bb02eebf51616f6a65067 /src/nat.ts | |
| download | ts-theorem-provinator-f6e26212620de411e082cbd52379075ea5a99032.tar.gz ts-theorem-provinator-f6e26212620de411e082cbd52379075ea5a99032.zip | |
init commit rewriting shit
Diffstat (limited to 'src/nat.ts')
| -rw-r--r-- | src/nat.ts | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/nat.ts b/src/nat.ts new file mode 100644 index 0000000..86bd318 --- /dev/null +++ b/src/nat.ts @@ -0,0 +1,16 @@ +declare const prev: unique symbol + +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 _0 = 0 & { [prev]: null } +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> |