fun operator ∘<T, U, V>(g:(fn U -> V), f:(fn T -> U)) {
fun x:T {
g(f(x))
}
}
fun update<T, U>(f:(fn T -> U), x:T, v:U) {
fun y:T {
if y = x then
v
else
f(y)
}
}
update_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U. update(f, x, v)(x) = v))
update_not_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, y:T. (if not (x = y) then update(f, x, v)(y) = f(y))))
update_shadow: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U. update(update(f, x, v), x, w) = update(f, x, w)))
update_permute: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U, y:T. (if not (x = y) then update(update(f, x, v), y, w) = update(update(f, y, w), x, v))))
fun empty_map<T, U>(k:T) {
@none<U>
}
fun domain<T, U>(f:(fn T -> Option<U>)) {
char_fun(fun x:T { switch f(x) { case none { false } case just(y) { true } } })
}
fun restrict<T, U>(f:(fn T -> Option<U>), P:Set<T>) {
fun x:T {
if x ∈ P then
f(x)
else
@none<U>
}
}
fun combine<T, U>(f:(fn T -> Option<U>), g:(fn T -> Option<U>)) {
fun x:T {
if f(x) = none then
g(x)
else
f(x)
}
}
combine_left: (all T:type, U:type, f:(fn T -> Option<U>), g:(fn T -> Option<U>), x:T. (if g(x) = none then combine(f, g)(x) = f(x)))
combine_right: (all T:type, U:type, f:(fn T -> Option<U>), g:(fn T -> Option<U>), x:T. (if f(x) = none then combine(f, g)(x) = g(x)))
restrict_domain: (all T:type, U:type. (all f:(fn T -> Option<U>), P:Set<T>. domain(restrict(f, P)) ⊆ P))
fun flip<T, U, V>(f) {
fun x, y {
f(y, x)
}
}
flip_flip: (all T:type. (all f:(fn T, T -> T). flip(flip(f)) = f))