Division
This commit is contained in:
+7
-1
@@ -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));
|
||||
|
||||
|
||||
Reference in New Issue
Block a user