Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/gears.agda.replaced @ 2:c7acb9211784
add code, figure. and paper fix content
author | ryokka |
---|---|
date | Mon, 27 Jan 2020 20:41:36 +0900 |
parents | |
children | b5fffa8ae875 |
line wrap: on
line source
proofGears : {c10 : @$\mathbb{N}$@ } → Set proofGears {c10} = whileTest {_} {_} {c10} (@$\lambda$@ n p1 → conversion1 n p1 (@$\lambda$@ n1 p2 → whileLoop' n1 p2 (@$\lambda$@ n2 → ( vari n2 @$\equiv$@ c10 ))))