cw.bend source

cw.bend on the hub · documented module

import Basedef ap(h: (Nat -> Nat) -> Nat -> Nat, s: Nat -> Nat, n: Nat) -> Nat:  h(s)(n)def qof(f: (Nat -> Nat) -> Nat -> Nat) -> Quant:  &1def k(f: (Nat -> Nat) -> Nat -> Nat, g: Nat -> Nat, -A: Kind(qof(f)), b: Bool) -> Nat:  match b:    case True{}:      ap(f, (x => x), 0n)    case False{}:      g(1n)def main() -> Nat:  k((y => y), (x => 5n), Unit, True{})