Mercurial > hg > Papers > 2020 > ryokka-sigss

view src/sound-psemcom.agda.replaced @ 0:85ee6174f90a default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add paper
author ryokka
date Wed, 12 Feb 2020 17:55:00 +0900
parents
children
line wrap: on
line source

whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ 
  output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) 
  @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
whileTestPSemSound c output refl = whileTestPSem c