def binpow_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/float.bend:103

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N

103# k = 0 is a fixed point of the specification's loop
104def binpow_zero(~T: Data, ~op: N.Op<T> -> T, fuel: Nat, +b: T, +a: T) -> {SG.binpow(~T, ~op, fuel, 0n, b, a) == a : T}:
105  match fuel:
106    case 0n:
107      {==}
108    case 1n+f:
109      binpow_zero(~T, ~op, f, b, a)