Add testL5cons00data

shingarov · Nov 4, 2024 · 45bdb26 · 45bdb26
1 parent b4c3d1b
commit 45bdb26
Showing 1 changed file with 26 additions and 0 deletions.
diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
@@ -746,6 +746,32 @@ SpriteHornPosTest >> testL5cons00 [
 
 ]
 
+{ #category : #'tests-L5' }
+SpriteHornPosTest >> testL5cons00data [
+	self provePos: '
+(var $k3 ((`a) ((L `a)) (`a)))
+(var $k1 ((`a) (`a)))
+
+(constant len (func(1 , [(L @(0)); int])))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+  (forall ((x `a) (Bool true))
+   (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))))
+       ((((len value: v) === 1))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5foldRight00 [
 	self provePos: '