Mercurial > hg > Members > soto > experimental

changeset 12:77f0530f2eff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix typo
author soto
date Thu, 11 Feb 2021 17:30:33 +0900
parents e6a7215fb00c
children 724766af8b12
files WhileTest.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/WhileTest.agda	Thu Feb 11 17:23:49 2021 +0900
+++ b/WhileTest.agda	Thu Feb 11 17:30:33 2021 +0900
@@ -37,8 +37,8 @@
     env : Env
   whileInit :  {m : Level }  {t : Set m } → (c10 : ℕ) → (Env → t) → t
   whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
-  whileInit-imple : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) )
-  whileInit-imple c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
+  whileInit-impl : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) )
+  whileInit-impl c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
   whileLoop : Env → (Code : Env → t) → t
   whileLoop env next = whileLoop1 (varn env) env where
       whileLoop1 : ℕ → Env → t