Contents

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

Version data entries

16 entries across 16 versions & 2 rubygems

Version	Path
rouge-4.5.1	lib/rouge/demos/lean
rouge-4.5.0	lib/rouge/demos/lean
rouge-4.4.0	lib/rouge/demos/lean
rouge-4.3.0	lib/rouge/demos/lean
rouge-4.2.1	lib/rouge/demos/lean
rouge-4.2.0	lib/rouge/demos/lean
rouge-4.1.3	lib/rouge/demos/lean
rouge-4.1.2	lib/rouge/demos/lean
rouge-4.1.1	lib/rouge/demos/lean
mumukit-content-type-1.12.1	vendor/bundle/ruby/2.7.0/gems/rouge-3.30.0/lib/rouge/demos/lean
mumukit-content-type-1.12.0	vendor/bundle/ruby/2.7.0/gems/rouge-3.30.0/lib/rouge/demos/lean
rouge-4.1.0	lib/rouge/demos/lean
rouge-4.0.1	lib/rouge/demos/lean
rouge-4.0.0	lib/rouge/demos/lean
rouge-3.30.0	lib/rouge/demos/lean
rouge-3.29.0	lib/rouge/demos/lean