view paper/src/AgdaPlus.agda.replaced @ 2:c7acb9211784

add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
line wrap: on
line source

_+_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Nat
zero  + m = m
suc n + m = suc (n + m)