diff Paper/src/while_loop_impl/while_loop_c.agda.replaced @ 5:339fb67b4375

INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents 9176dff8f38a
children
line wrap: on
line diff
--- a/Paper/src/while_loop_impl/while_loop_c.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/while_loop_impl/while_loop_c.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,2 +1,2 @@
-whileLoopC : @$\mathbb{N}$@ @$\rightarrow$@ Env
-whileLoopC n = whileTest n (@$\lambda$@ env @$\rightarrow$@ whileLoop env (@$\lambda$@ env1 @$\rightarrow$@ env1 ))
\ No newline at end of file
+whileLoopC : !$\mathbb{N}$! !$\rightarrow$! Env
+whileLoopC n = whileTest n (!$\lambda$! env !$\rightarrow$! whileLoop env (!$\lambda$! env1 !$\rightarrow$! env1 ))
\ No newline at end of file