add ignored test for nested Real definitions

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java

@@ -115,4 +115,17 @@ public class TestModuleNaturals {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testNestedDefinitions() throws Exception {
+		String module = "---- MODULE Testing ----\n"
+				+ "EXTENDS Naturals \n"
+				+ "InnerDef(b) == b*5 \n"
+				+ "HelpDef(a,b) == a+b \n"
+				+ "Init == 1 = HelpDef(1,1) \n"
+				+ "===============";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("INTEGER", t.getDefinitionType("HelpDef"));
+		assertEquals("INTEGER", t.getDefinitionType("InnerDef"));
+	}
+
 }

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java

@@ -4,11 +4,11 @@ import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.exceptions.TypeErrorException;
 import de.tla2b.util.TestTypeChecker;
 import de.tla2b.util.TestUtil;
+import org.junit.Ignore;
 import org.junit.Test;
 
 import static org.junit.Assert.assertEquals;
 
-
 public class TestModuleReals {
 
 	/*
@@ -172,4 +172,19 @@ public class TestModuleReals {
 			+ "=================================";
 		TestUtil.typeCheckString(module);
 	}
+
+	@Ignore
+	@Test
+	public void testNestedDefinitions() throws Exception {
+		// FIXME: this fails because the default type is Int and we first type everything as Int
+		String module = "---- MODULE Testing ----\n"
+				+ "EXTENDS Reals \n"
+				+ "InnerDef(b) == b*5.0 \n"
+				+ "HelpDef(a,b) == a+InnerDef(b) \n"
+				+ "Init == 1.0 = HelpDef(1.0,1.0) \n"
+				+ "===============";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("REAL", t.getDefinitionType("HelpDef"));
+		assertEquals("REAL", t.getDefinitionType("InnerDef"));
+	}
 }