Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/gears.agda @ 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
proofGears : {c10 : ℕ } → Set proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))