More fixes

ajreynol · Feb 19, 2025 · 6197036 · 6197036
1 parent 47d649b
commit 6197036
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/proofs/eo/cpc/programs/SeqToString.eo b/proofs/eo/cpc/programs/SeqToString.eo
@@ -89,7 +89,6 @@
 (program $seq_to_string_op_rec ((U Type) (T Type) (f (-> T U)) (b T) (units @List) (chars @List) (S Type) (V Type) (u V) (ts (Seq V) :list))
   (T @List @List) (Tuple S @List @List)
   (
-  (($seq_to_string_op_rec (seq.++ (seq.unit u) ts) units chars) ($seq_to_string_rec (seq.++ (seq.unit u) ts) "" units chars (eo::list_len @list units)))
   (($seq_to_string_op_rec (seq.unit u) units chars)             ($seq_to_string_rec (seq.unit u) "" units chars (eo::list_len @list units)))
   (($seq_to_string_op_rec (@seq.empty (Seq V)) units chars)     (tuple "" units chars))
   (($seq_to_string_op_rec (f b) units chars)                    (eo::match ((S1 Type) (fs S1) (nunits1 @List) (nchars1 @List))

diff --git a/proofs/eo/cpc/rules/Strings.eo b/proofs/eo/cpc/rules/Strings.eo
@@ -883,7 +883,7 @@
   (
     ; handle sequence-specific operators here
     (($seq_eval (seq.nth t n))  (eo::match ((e T))
-                                  (eo::list_nth str.++ t n)
+                                  (eo::list_nth str.++ ($str_to_nary_form t false) n)
                                   (((seq.unit e) e))))
     ; otherwise, we rely on the strings evaluator
     (($seq_eval t)              (eo::match ((S Type) (u S) (units @List) (chars @List))