a0d42e7709
no zoom yet, also no figuring out when tree nodes can merge without losing information.
24 lines
404 B
JavaScript
24 lines
404 B
JavaScript
// OPTION TYPE
|
|
|
|
/*
|
|
usage:
|
|
None().none(f1).some(f2) // returns f1()
|
|
Some(x).none(f1).some(f2) // returns f2(x)
|
|
None(x).unwrap(y) // returns y
|
|
Some(x).unwrap(y) // returns x
|
|
*/
|
|
|
|
export function None() {
|
|
return {
|
|
none: (f) => f(),
|
|
some: (f) => None(),
|
|
unwrap: (y) => y,
|
|
};
|
|
}
|
|
export function Some(x) {
|
|
return {
|
|
none: (f) => Some(x),
|
|
some: (f) => f(x),
|
|
unwrap: (y) => x,
|
|
};
|
|
}
|