more experiments with SpriteHornTests re: data

shingarov · Sep 20, 2024 · b555d36 · b555d36
1 parent 6dec464
commit b555d36
Showing 1 changed file with 22 additions and 4 deletions.
diff --git 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: '