next up previous contents index
Next: Tactics in ML Up: An Overview of Previous: Syntax and Semantics

Using ML in Nuprl

ML   can be used in conjunction with the Nuprl system in a variety of ways. The easiest way to invoke ML is to give the command ml in the command window; this invokes an interactive ML  interpreter. Expressions for evaluation are typed at the M> prompt  and ended with ;; followed by a carriage return. Figure gif illustrates some examples of using ML from the Nuprl command window. The user's input is on lines indicated with M>, while the system responds on the line below with the value of the expression (except when the expression is a function) and the type of the expression. Note how a polymorphic expression is typed in the third example.

Another way to invoke ML is to use the create command to create an object of ML type as in the following example.

        create m1 ml top
One can then invoke the text editor  on the object using the view command. The body of an ML program can be written, and the result can be checked using the check command in the Nuprl command window. This process is illustrated in figure gif.

Figure: Examples of ML Expressions with Their Inferred Types

Figure: Using the Text Editor to Write ML Programs


Richard Eaton
Thu Sep 14 08:45:18 EDT 1995