def bends

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

import Base

129def bends(f: Nat, +n: Nat) -> Bool:
130  match f n:
131    case 0n 0n:
132      True{}
133    case 0n 1n+np:
134      False{}
135    case 1n+g 0n:
136      True{}
137    case 1n+g 1n+ +np:
138      bends(g, Nat.div(1n+np, 2n))