def ud.pred

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:18

import Base

18def ud.pred(n: Nat) -> Nat:
19  match n:
20    case 0n:
21      0n
22    case 1n+p:
23      p