Mercurial > hg > Papers > 2019 > ryokka-sigss
view Paper/src/gears.agda.replaced @ 8:83d000399c9d
fix invisible char
author | ryokka |
---|---|
date | Tue, 18 Dec 2018 04:08:28 +0900 |
parents | |
children |
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 ))))