def nat.dbit

bend-osdev-algo@0.1.0.0 · PROOF.bend:856

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

856def nat.dbit(b: Bool, a: Nat) -> Nat:
857  match b:
858    case False{}:
859      Nat.double(a)
860    case True{}:
861      1n+Nat.double(a)

Uses (3)

Used by (2)