test nested boolean

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