Reverse a string: Difference between revisions

Content deleted Content added

Inline

@@ Line 272: / Line 272: @@
 =={{header|Agda}}==
-Using the Agda standard library, version 0.6.
+Using the Agda standard library, version 1.7 .
-<syntaxhighlight lang="agda2">module reverse_string where
+<syntaxhighlight lang="agda">
+module ReverseString where
-open import Data.String
+open import Data.String using (String ; fromList ; toList)
-open import Data.List
+open import Data.List using (reverse)
-reverse_string : String → String
+reverse-string : String → String
-reverse_string s = fromList (reverse (toList s))</syntaxhighlight>
+reverse-string s = fromList (reverse (toList s))
+</syntaxhighlight>
 =={{header|Aime}}==