Remove outdated note from :type command help

ProB now returns the types in B syntax rather than internal Prolog terms.

Remove outdated note from :type command help
1c8f4ecb · dgelessus · bbc147f3 · 1c8f4ecb · 1c8f4ecb
Commit 1c8f4ecb authored 5 years ago by dgelessus
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -12,15 +12,11 @@
       ":type FORMULA\n",
       "```\n",
       "\n",
-       "Display the type of a formula.\n",
-       "\n",
-       "The returned types are *not* standard B types. They are human-readable, but cannot be used in code."
+       "Display the type of a formula."
      ],
      "text/plain": [
       ":type FORMULA\n",
-       "Display the type of a formula.\n",
-       "\n",
-       "The returned types are *not* standard B types. They are human-readable, but cannot be used in code."
+       "Display the type of a formula."
      ]
     },
     "execution_count": 1,

 %% Cell type:code id: tags:

 ``` prob
 :help :type
 ```

 %% Output

    ```
    :type FORMULA
    ```
    
    Display the type of a formula.
-    
-    The returned types are *not* standard B types. They are human-readable, but cannot be used in code.
    :type FORMULA
    Display the type of a formula.
-    
-    The returned types are *not* standard B types. They are human-readable, but cannot be used in code.

 %% Cell type:markdown id: tags:

 `:type` works on expressions.

 %% Cell type:code id: tags:

 ``` prob
 :type 1
 ```

 %% Output

    INTEGER

 %% Cell type:code id: tags:

 ``` prob
 :type {}
 ```

 %% Output

    POW(?)

 %% Cell type:code id: tags:

 ``` prob
 :type {1, 2, 3}
 ```

 %% Output

    POW(INTEGER)

 %% Cell type:code id: tags:

 ``` prob
 :type 1..5
 ```

 %% Output

    POW(INTEGER)

 %% Cell type:code id: tags:

 ``` prob
 :type [1, 2, 3]
 ```

 %% Output

    seq(INTEGER)

 %% Cell type:code id: tags:

 ``` prob
 :type {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}
 ```

 %% Output

    POW(((INTEGER*INTEGER)<->INTEGER))

 %% Cell type:markdown id: tags:

 `:type` works on predicates.

 %% Cell type:code id: tags:

 ``` prob
 :type 1 = 1
 ```

 %% Output

    predicate

 %% Cell type:code id: tags:

 ``` prob
 :type #x.(x : INT & x > 1)
 ```

 %% Output

    predicate

 %% Cell type:markdown id: tags:

 `:type` displays type errors.

 %% Cell type:code id: tags:

 ``` prob
 :type {1, TRUE, "string", {}}
 ```

 %% Output

    Error from ProB: Type errors in formula
    3 errors:
    Error: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)
    // Source code not known
    Error: Type mismatch: Expected INTEGER, but was STRING in '"string"' (:1:10 to 1:18)
    // Source code not known
    Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)
    // Source code not known

 %% Cell type:code id: tags:

 ``` prob
 :type 1 + {}
 ```

 %% Output

    Error from ProB: Type errors in formula
    Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)
    // Source code not known

 %% Cell type:markdown id: tags:

 Local variables can be passed to `:type`.

 %% Cell type:code id: tags:

 ``` prob
 :let thing {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}
 ```

 %% Output

    $\{\{(1\mapsto 2\mapsto 3),(4\mapsto 5\mapsto 6)\},\{(7\mapsto 8\mapsto 9)\}\}$
    {{(1↦2↦3),(4↦5↦6)},{(7↦8↦9)}}

 %% Cell type:code id: tags:

 ``` prob
 :type thing
 ```

 %% Output

    POW(((INTEGER*INTEGER)<->INTEGER))

 %% Cell type:code id: tags:

 ``` prob
 :type thing, 123
 ```

 %% Output

    POW(((INTEGER*INTEGER)<->INTEGER))*INTEGER

--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -41,7 +41,7 @@ public final class TypeCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "The returned types are *not* standard B types. They are human-readable, but cannot be used in code.";
+		return "";
 	}
 	
 	@Override