This commit is contained in:
Freywar Ulvnaudgari
2024-08-05 19:53:04 +03:00
parent b2a69c8ea1
commit 9e57810aa8
2 changed files with 60 additions and 2 deletions
+7 -1
View File
@@ -1,6 +1,6 @@
import { toNative as $$, L, P, _, fromNative as __, id } from './core';
import { EQ, GT, LT, Ord } from './ord';
import { Bool, False, True } from './bool';
import { Bool, False, iif, True } from './bool';
export type Num = L<<T extends P>(z: T) => L<(n: L<(p: Num) => T>) => T>>;
@@ -52,6 +52,12 @@ export const sub: L<(l: Num) => L<(r: Num) => Num>>
export const mul: L<(l: Num) => L<(r: Num) => Num>>
= _(l => _(r => l._(Zero)._(_(pl => sum._(r)._(mul._(pl)._(r))))));
export const div: L<(l: Num) => L<(r: Num) => Num>>
= _(l => _(r => iif._(lt._(l)._(r))._(Zero)._(succ._(div._(sub._(l)._(r))._(r)))));
export const mod: L<(l: Num) => L<(r: Num) => Num>>
= _(l => _(r => iif._(lt._(l)._(r))._(l)._(mod._(sub._(l)._(r))._(r))));
export const fromNumber: (n: number) => Num
= n => !n ? Zero : Succ._(new L(() => fromNumber(n - 1).value));