--- a/Paper/src/AgdaStackImpl.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/AgdaStackImpl.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,4 +1,4 @@
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} !$\rightarrow$! SingleLinkedStack Data !$\rightarrow$! Data !$\rightarrow$! (Code : SingleLinkedStack Data !$\rightarrow$! t) !$\rightarrow$! t
 pushSingleLinkedStack stack datum next = next stack1
   where
     element = cons datum (top stack)
@@ -6,13 +6,13 @@
 
 -- Basic stack implementations are specifications of a Stack
 
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} !$\rightarrow$! StackMethods {n} {m} a {t} (SingleLinkedStack a)
 singleLinkedStackSpec = record {
                            push = pushSingleLinkedStack
                          ; pop  = popSingleLinkedStack
                          }
 
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} !$\rightarrow$! Stack {n} {m} a {t} (SingleLinkedStack a)
 createSingleLinkedStack = record {
                         stack = emptySingleLinkedStack ;
                         tackMethods = singleLinkedStackSpec