def pred

lawful-arrays@0.1.0.0 · proof_base.bend:84

import Base

84def pred(n: Nat) -> Nat:
85  match n:
86    case 0n:
87      0n
88    case 1n+p:
89      p