view int ::= Zero | Succ int in n = Zero, if n = 0 = Succ (n - 1), if n > 0 out Zero = 0 out (Succ n) = n + 1You can then pattern match on the Peano data types as if you were working with integers and GuardClauses. For example, you could define exponentiation as
power x Zero = 1 power x (Succ n) = x * power x nAnd you could define Fibonacci numbers as:
fib Zero = Zero fib (Succ Zero) = Succ Zero fib (Succ (Succ n)) = (fib n) + (fib (Succ n))I'm not sure if this is implemented in any production language. The paper is written in pseudo-MirandaLanguage, and IIRC there have been proposals to add it to HaskellLanguage.