# HG changeset patch
# User soto
# Date 1613032233 -32400
# Node ID 77f0530f2eff2ca318d63e5b5a4e7cdc3b289143
# Parent  e6a7215fb00c5400c14e7700a435daaec4f14602
fix typo

diff -r e6a7215fb00c -r 77f0530f2eff WhileTest.agda
--- 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