Update translation of Seq constructor

examples/src/main/scala/soda/example/forlean/algorithms/Recursion.lean

@@ -34,7 +34,7 @@ private def   _tailrec_foldl_while ( A : Type ) ( B : Type ) (sequence : List (
        (next : B -> A -> B) (condition : B -> A -> Bool) : B :=
     match sequence with
       | List.nil => current
-      | (head) +: (tail) =>
+      | (head) :: (tail) =>
         if (not (condition (current) (head) ) )
         then current
         else _tailrec_foldl_while ( A ) ( B ) (tail) (next (current) (head) ) (next) (condition)
@@ -64,7 +64,7 @@ private def   _tailrec_foldl ( A : Type ) ( B : Type ) (sequence : List ( A ) )
        (next : B -> A -> B) : B :=
     match sequence with
       | List.nil => current
-      | (head) +: (tail) =>
+      | (head) :: (tail) =>
         _tailrec_foldl ( A ) ( B ) (tail) (next (current) (head) ) (next)
 
 
@@ -90,7 +90,7 @@ namespace Range
  private def   _tailrec_range (non_negative_number : Int) (sequence : List ( Int ) ) : List ( Int ) :=
     match non_negative_number with
       | Succ_ (k) =>
-        _tailrec_range (k) ( (k) +: (sequence) )
+        _tailrec_range (k) ( (k) :: (sequence) )
       | _otherwise => sequence
 
 

translator/src/main/scala/soda/translator/extension/tolean/LeanClassConstructorBlockTranslator.soda

@@ -63,7 +63,7 @@ class LeanClassConstructorBlockTranslator
     _tc .lean_new_line + _get_initial_spaces (beginning) + _two_spaces +
     _tc .lean_default_constructor_name +
     _tc .lean_space +
-    _tc .lean_constructor_symbol +
+    _tc .lean_list_constructor_symbol +
     _tc .lean_new_line + _get_initial_spaces (beginning) + _four_spaces +
     functions .mkString (_tc .lean_new_line + _get_initial_spaces (beginning) + _four_spaces) +
     _tc .lean_new_line +

translator/src/main/scala/soda/translator/extension/tolean/Package.scala

@@ -135,7 +135,7 @@ trait LeanClassConstructorBlockTranslator
     _tc .lean_new_line + _get_initial_spaces (beginning) + _two_spaces +
     _tc .lean_default_constructor_name +
     _tc .lean_space +
-    _tc .lean_constructor_symbol +
+    _tc .lean_list_constructor_symbol +
     _tc .lean_new_line + _get_initial_spaces (beginning) + _four_spaces +
     functions .mkString (_tc .lean_new_line + _get_initial_spaces (beginning) + _four_spaces) +
     _tc .lean_new_line +
@@ -1226,7 +1226,7 @@ trait TranslationConstantToLean
 
   lazy val lean_product_type_symbol = "*"
 
-  lazy val lean_constructor_symbol = "::"
+  lazy val lean_list_constructor_symbol = "::"
 
   lazy val lean_lambda_arrow_symbol = "=>"
 
@@ -1626,8 +1626,8 @@ trait TranslationConstantToLean
       Tuple2 (soda_constant .or_reserved_word , lean_or_symbol) ,
       Tuple2 (soda_constant .tail_recursion_annotation , lean_empty_string) ,
       Tuple2 (soda_constant .override_annotation , lean_empty_string) ,
-      Tuple2 (soda_constant .new_annotation , lean_empty_string)
-
+      Tuple2 (soda_constant .new_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .seq_constructor_symbol , lean_list_constructor_symbol)
     )
 
   lazy val type_translation : Seq [Tuple2 [String, String]  ] =

translator/src/main/scala/soda/translator/extension/tolean/TranslationConstantToLean.soda

@@ -56,7 +56,7 @@ class TranslationConstantToLean
 
   lean_product_type_symbol = "*"
 
-  lean_constructor_symbol = "::"
+  lean_list_constructor_symbol = "::"
 
   lean_lambda_arrow_symbol = "=>"
 
@@ -456,8 +456,8 @@ class TranslationConstantToLean
       Tuple2 (soda_constant .or_reserved_word , lean_or_symbol) ,
       Tuple2 (soda_constant .tail_recursion_annotation , lean_empty_string) ,
       Tuple2 (soda_constant .override_annotation , lean_empty_string) ,
-      Tuple2 (soda_constant .new_annotation , lean_empty_string)
-
+      Tuple2 (soda_constant .new_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .seq_constructor_symbol , lean_list_constructor_symbol)
     )
 
   type_translation : Seq [Tuple2 [String] [String]  ] =

translator/src/main/scala/soda/translator/extension/toscala/Package.scala

@@ -1501,6 +1501,8 @@ trait TranslationConstantToScala
 
   lazy val scala_or_symbol = "||"
 
+  lazy val scala_empty_list_reserved_word = "Nil"
+
   lazy val scala_tail_recursion_annotation_translation =
     "import scala.annotation.tailrec\n        @tailrec  final"
 

translator/src/main/scala/soda/translator/extension/toscala/TranslationConstantToScala.soda

@@ -95,6 +95,8 @@ class TranslationConstantToScala
 
   scala_or_symbol = "||"
 
+  scala_empty_list_reserved_word = "Nil"
+
   scala_tail_recursion_annotation_translation =
     "import scala.annotation.tailrec\n        @tailrec  final"
 

translator/src/main/scala/soda/translator/parser/Package.scala

@@ -515,6 +515,8 @@ trait SodaConstant
 
   lazy val list_constructor_unicode_symbol = "\u2237"
 
+  lazy val seq_constructor_symbol = "+:"
+
   lazy val documentation_comment_opening_symbol = "/**"
 
   lazy val comment_opening_symbol = "/*"

translator/src/main/scala/soda/translator/parser/SodaConstant.soda

@@ -169,6 +169,8 @@ class SodaConstant
 
   list_constructor_unicode_symbol = "\u2237"
 
+  seq_constructor_symbol = "+:"
+
   documentation_comment_opening_symbol = "/**"
 
   comment_opening_symbol = "/*"

translator/src/test/resources/soda/translator/example/forlean/algorithms/Recursion.lean

@@ -34,7 +34,7 @@ private def   _tailrec_foldl_while ( A : Type ) ( B : Type ) (sequence : List (
        (next : B -> A -> B) (condition : B -> A -> Bool) : B :=
     match sequence with
       | List.nil => current
-      | (head) +: (tail) =>
+      | (head) :: (tail) =>
         if (not (condition (current) (head) ) )
         then current
         else _tailrec_foldl_while ( A ) ( B ) (tail) (next (current) (head) ) (next) (condition)
@@ -64,7 +64,7 @@ private def   _tailrec_foldl ( A : Type ) ( B : Type ) (sequence : List ( A ) )
        (next : B -> A -> B) : B :=
     match sequence with
       | List.nil => current
-      | (head) +: (tail) =>
+      | (head) :: (tail) =>
         _tailrec_foldl ( A ) ( B ) (tail) (next (current) (head) ) (next)
 
 
@@ -90,7 +90,7 @@ namespace Range
  private def   _tailrec_range (non_negative_number : Int) (sequence : List ( Int ) ) : List ( Int ) :=
     match non_negative_number with
       | Succ_ (k) =>
-        _tailrec_range (k) ( (k) +: (sequence) )
+        _tailrec_range (k) ( (k) :: (sequence) )
       | _otherwise => sequence
 
 

translator/src/test/scala/soda/translator/extension/tolean/MicroTranslatorToLeanSpec.soda

@@ -213,19 +213,35 @@ class MicroTranslatorToLeanSpec ()
     check (
       obtained := instance .translate (
         "as_list (a : Boolean) : List [Boolean] =" +
-        "\n  (a) :: (Nil)" +
+        "\n  a :: Nil" +
         "\n"
       )
     ) (
       expected := "" +
         " def as_list (a : Bool) : List ( Bool ) :=" +
-        "\n  (a) :: (List.nil)" +
+        "\n  a :: List.nil" +
         "\n" +
         "\n"
     )
   )
 
   test ("Lean translation of types 2") (
+    check (
+      obtained := instance .translate (
+        "as_seq (a : Boolean) : Seq [Boolean] =" +
+        "\n  (a) +: (Nil)" +
+        "\n"
+      )
+    ) (
+      expected := "" +
+        " def as_seq (a : Bool) : List ( Bool ) :=" +
+        "\n  (a) :: (List.nil)" +
+        "\n" +
+        "\n"
+    )
+  )
+
+  test ("Lean translation of types 3") (
     check (
       obtained := instance .translate (
         "class Example" +

translator/src/test/scala/soda/translator/extension/tolean/Package.scala

@@ -292,19 +292,35 @@ case class MicroTranslatorToLeanSpec ()
     check (
       obtained = instance .translate (
         "as_list (a : Boolean) : List [Boolean] =" +
-        "\n  (a) :: (Nil)" +
+        "\n  a :: Nil" +
         "\n"
       )
     ) (
       expected = "" +
         " def as_list (a : Bool) : List ( Bool ) :=" +
-        "\n  (a) :: (List.nil)" +
+        "\n  a :: List.nil" +
         "\n" +
         "\n"
     )
   )
 
   test ("Lean translation of types 2") (
+    check (
+      obtained = instance .translate (
+        "as_seq (a : Boolean) : Seq [Boolean] =" +
+        "\n  (a) +: (Nil)" +
+        "\n"
+      )
+    ) (
+      expected = "" +
+        " def as_seq (a : Bool) : List ( Bool ) :=" +
+        "\n  (a) :: (List.nil)" +
+        "\n" +
+        "\n"
+    )
+  )
+
+  test ("Lean translation of types 3") (
     check (
       obtained = instance .translate (
         "class Example" +