From 89da5dd3c04142b60dea8368627826d540d7a339 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Sun, 3 Nov 2024 19:57:44 -0500
Subject: [PATCH] Add testL5cons00data

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

diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
index c022fd19b..b4ce523ff 100644
--- 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: '