def fv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:907

import Base

907# y when ok, else x: {fv(ok, v(a), x) == x} says v(a) == x when ok
908def fv(ok: Bool, +y: Nat, +x: Nat) -> Nat:
909  match ok:
910    case True{}:
911      y
912    case False{}:
913      x