From b555d368ebf4de08bd314cb9468a2dda29c3d731 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Fri, 20 Sep 2024 03:48:36 -0400
Subject: [PATCH] more experiments with SpriteHornTests re: data

---
 .../SpriteHornPosTest.class.st                | 26 ++++++++++++++++---
 1 file changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
index 3ff7acffa..a22534202 100644
--- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st
+++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
@@ -749,10 +749,10 @@ SpriteHornPosTest >> testL5cons00 [
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5cons00data [
 	self provePos: '
-(var $k3 ((`a) ((`L `a)) (`a)))
+(var $k3 ((`a) ((L `a)) (`a)))
 (var $k1 ((`a) (`a)))
 
-(constant len (func(1 , [(`L @(0)); int])))
+(constant len (func(1 , [(L @(0)); int])))
 
 (data L 1 = [
         | Nil {}
@@ -761,13 +761,13 @@ SpriteHornPosTest >> testL5cons00data [
 
 (constraint
   (forall ((x `a) (Bool true))
-   (forall ((t (`L `a)) ((len value: t) === 0))
+   (forall ((t (L `a)) ((len value: t) === 0))
      (and
       (forall ((VV `a) (VV === x))
        (($k3 VV t x)))
       (forall ((VV0 `a)  ($k1 VV0 x))
         (($k3 VV0 a x)))
-      (forall ((v (`L `a)) ((len value: v) === (1 + (len value: t))))
+      (forall ((v (L `a)) ((len value: v) === (1 + (len value: t))))
        ((((len value: v) === 1))))))))
 '
 
@@ -1171,6 +1171,24 @@ SpriteHornPosTest >> testL5tail01 [
 
 ]
 
+{ #category : #'tests-L5' }
+SpriteHornPosTest >> testL5tail01L8 [
+	self provePos: '
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constant len (func(1 , [(L @(0)); int])))
+
+(constraint
+  (forall ((h `a) (Bool true))
+    (forall ((t (L `a)) (Bool true))
+      (forall ((zs (L `a)) (and ((len value: zs) > 0)  ((len value: zs) === (1 + (len value: t)))))
+        (forall ((VV (L `a)) (VV === t)) ((((len value: VV) === ((len value: zs) - 1)))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5tuple00 [
 	self provePos: '