def pred
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as Natimport Base
10def pred(n: Nat) -> Nat:
11 match n:
12 case 0n:
13 0n
14 case 1n+p:
15 p
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as Natimport Base
10def pred(n: Nat) -> Nat:
11 match n:
12 case 0n:
13 0n
14 case 1n+p:
15 p