def ends

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:30

import Base

30# the Nat loop reaches b == 0 within f steps
31def ends(f: Nat, +a: Nat, +b: Nat) -> Bool:
32  match f b:
33    case 0n 0n:
34      True{}
35    case 0n 1n+bp:
36      False{}
37    case 1n+g 0n:
38      True{}
39    case 1n+g 1n+ +bp:
40      ends(g, 1n+bp, Nat.mod(a, 1n+bp))