def ns.pred

bend-osdev-word64@0.1.1.0 · proof_shift.bend:41

import Base

41def ns.pred(x: Nat) -> Nat:
42  match x:
43    case 0n:
44      0n
45    case 1n+ +p:
46      p