path: root/vendor/bundle/ruby/3.4.0/gems/rouge-4.5.2/lib/rouge/demos/lean

open nat

def add : nat → nat → nat
| m zero := m
| m (succ n) := succ (add m n)

-- encode definition as an axiom
axiom add_zero (n : nat) : n + 0 = n