From 9796cb6e6ef5c6242f086534e6e7d85c5842103c Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Tue, 14 Jan 2025 14:08:32 +0100
Subject: [PATCH] test nested boolean
---
.../java/de/tla2b/typechecking/BBuiltInsTest.java | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index c282108..e0652e8 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -35,6 +35,18 @@ public class BBuiltInsTest {
assertEquals("POW(BOOL)", t.getConstantType("k"));
}
+ @Test
+ public void testNestedBooleanDefinitions() throws Exception {
+ String module = "---- MODULE Testing ----\n"
+ + "EXTENDS Naturals \n"
+ + "InnerDef(b) == b>5 \n"
+ + "HelpDef(a,b) == a<7 /\\ InnerDef(b) \n"
+ + "Init == TRUE = HelpDef(3,4) \n"
+ + "===============";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("BOOL", t.getDefinitionType("HelpDef"));
+ assertEquals("BOOL", t.getDefinitionType("InnerDef"));
+ }
/*
* String
--
GitLab