For starting a proof
(cm-z)}'(cm-z)}'| Key commands: | obref}' |
(continued from...doc for pfterms )
.
... 
<ml> use the command
| Introduction | Introductory Remarks | |||
| COM | doc_for_how_to |
Use the | ||
| COM | doc_for_intro | The nuprl_sfa interface to Nuprl (Nuprl4 now, Nuprl5 later) ... | ||
| COM | doc_for_getting_started |
| ||
| COM | doc_for_how_to_find_documentation | How to find Documentation and Definitions. Review pertinent commands? YES ... | ||
| COM | doc_for_printing_main_doc | The documents explaining this editor are meant for interactive use, but you may want offline hardcopy, especially if you are a new or prospective user. ... | ||
| COM | doc_for_user_specializing | Tailoring this Editor for the User. QUIT ... | ||
| COM | doc_for_using_pauls_manual |
Paul Jackson's | ||
| COM | doc_for_math_expression | Finding Explanations of Mathematical Expression in Nuprl ... | ||
| COM | doc_for_active_mouse |
There are two main uses for what we may call the active mouse, | ||
| COM | doc_for_point_focus | Point, Focus, Zoom ... | ||
| COM | doc_for_how_to_view_objects |
While there are various ways to view objects, the basic one is by | ||
| COM | doc_for_how_to_quit_objects |
The command | ||
| COM | doc_for_undo | How to Undo Changes to an Object. ... | ||
| COM | doc_for_display_suppression | More than one display form may be usable for the same term. ... | ||
| COM | doc_for_explode_form | Exploding a term generates another term that represents the main operator in a way that makes the operator structure explicitly viewable and editable. ... | ||
| COM | doc_for_edit_match | This function is designed as a utility for matching against terms using patterns that are easy to create, using the editor, by modifying samples and variants of the terms you want to match. ... | ||
| COM | doc_for_term_insertion |
You can delete the term at the point, i.e., replace it with a term-placeholder, with | ||
| COM | doc_for_string_editing | Terms have parts that are not themselves terms, rather they are strings, sometimes called operator-parameters since they are often conceived as parameterizing families of operators. ... | ||
| COM | doc_for_string_editing2 |
(Continued from | ||
| COM | doc_for_edit_context | Often edit commands are overloaded depending on the display-forms or operators the point is located on or in, and perhaps on the kind of object in which the command is being executed. ... | ||
| COM | doc_for_comment_insertion | Comments may be inserted in most terms, and they will be ignored when the system uses a term for special purposes. ... | ||
| COM | doc_for_ML_editing | The primary form of ML in this editor is "structured". ... | ||
| COM | doc_for_proof_editing | Editing Proofs as Terms. ... | ||
| COM | doc_for_proof_refinement |
Making Proof Steps. (For proof term structure For starting a proof | ||
| COM | doc_for_proof_refinement2 |
(continued from | ||
| COM | doc_for_WORDS_editing | The WORDS operators are formally meaningless devices for representing words, punctuation, and collections of terms with control of spacing for display. One often embeds other terms in WORDS to form documents or menus. ... | ||
| COM | doc_for_WORDS_pairing |
WORDS pairing operators. (continued from | ||
| COM | doc_for_term_sequences | In the Nuprl system, for many purposes a term sequence will be represented by a term, using a binary operator as the catenator. ... | ||
| COM | doc_for_abs_edit | Operator definitions are given in ABS objects of the library. ... | ||
| COM | doc_for_edit_adjust_op_form_by | Adjust lhs to make it a reasonable left-hand-side of an operator definition with right-hand-side rhs. ... | ||
| COM | doc_for_display_form_edit |
Display form specification can be rather complicated, so we will not give a complete explanation here. More documentation on display methods will be added in time. For more complicated methods of display, it is suggested that examples using those methods be found and emulated. The | ||
| COM | doc_for_display_form_imitation |
It is often easiest to imitate an example, rather than create from scratch. In the case of defining display forms, this is facilitated by the | ||
| COM | doc_for_display_form_models | Display Form Models. ... | ||
| COM | doc_for_display_form_formats | Display Form Formats. ... | ||
| COM | doc_for_display_form_dfchild | Display Form Child Formats. ... | ||
| COM | doc_for_display_form_dfchild_editing | Here we will discuss how to enter a display child format command. ... | ||
| COM | doc_for_display_form_attributes | Display Form "Attributes". ... | ||
| COM | doc_for_name_completion |
| ||
| COM | doc_for_toggling | In order to simplify transitions between closely related terms, there is a generic extensible toggle facility. These "toggles" typically cycle through several variations on a form of term. ... | ||
| COM | doc_for_term_search | How to search for terms in a window. ... | ||
| COM | doc_for_object_creation | How to create new objects and operator definitions. ... | ||
| COM | doc_for_ml_execution_cmds |
The main ways to invoke ML on user expressions are to use the commands (cm-z)}' | ||
| COM | doc_for_ml_execution_generic |
Executing ML code with | ||
| COM | doc_for_ml_execution_in_place |
Executing ML code with (cm-z)}' | ||
| COM | doc_for_ml_execution_mouse |
Executing ML code with | ||
| COM | doc_for_finding_lib_objects | Finding library objects. ... | ||
| COM | doc_for_ob_refs | Object Reference Terms, or obrefs. ... | ||
| COM | doc_for_ob_refs_editing | Editing Object Reference Terms ... | ||
| COM | doc_for_making_buttons |
| ||
| COM | doc_for_button_conversion_menu |
Note about limitations of button conversion. | ||
| COM | doc_for_cut_n_paste |
The basic concepts for insertion and deletion, and many of the commands are explained in | ||
| COM | doc_for_deptypeinsert | There is a standard method for flexible entry and editing of dependent type operators in Constable's standard notation. ... | ||
| COM | doc_for_posting_objects | Posting, Quitting, and Deleting Objects. ... | ||
| COM | doc_for_printing_object_sets | How to Print Collections of Nuprl Objects ... | ||
| COM | doc_for_ml_doc | How to find documentation and definitions for global ML ids. ... | ||
| COM | doc_for_kbd_cmd_nomenclature | Keyboard Command References. ... | ||
| COM | doc_for_xwindow_setup | X-windows setup ... | ||
| COM | doc_for_pfterms |
This editor is designed to edit entire proofs as terms. For advice on editing proof terms, see | ||
| COM | doc_for_pfterms2 |
(continued from... | ||
| COM | doc_for_edit_cmd_review | Normally, a keyboard command is associated with some documentation and an object specifying what keyboard string is bound to that command. ... | ||
| COM | doc_for_edit_cmd_review2 |
(continued from | ||
| COM | doc_for_ML_scanner |
Unstructured ML and the underlying scanner. (also | ||
| COM | doc_for_ML_editing_let | Editing Let Forms. ... | ||
| COM | doc_for_ML_editing_if | Editing If and Loop Forms. ... | ||
| COM | doc_for_thm_posting | THM objects versus proof terms. ... | ||
| COM | doc_for_abs_verify |
When an operator definition or declaration, an ABS object, is "verified" with the | ||
| COM | doc_for_edit_choice |
Sometimes the editor will provide a list of options in place, by presenting those options in a sequence connected with | ||
| COM | doc_for_insert_buttons |
The command .
... | ||
| COM | doc_for_ml_buttons |
To insert FN<ml> use the command | ||
| COM | doc_for_cmd_string_edit | The representation for command strings used by this editor is as a word or sequence of words jammed together with <words go here><words go here> with certain characters represented by special strings rather than themselves. ... | ||
| COM | doc_for_ops_as_macros | Not done yet. ... | ||
| COM | doc_for_proof_refinement_sample1 |
Example of method described in | ||
| COM | doc_for_201_display_kinds | This is a management device for controlling incompatible 201 display forms. ... | ||
| COM | doc_for_parentheses | Parenthesis Generation. ... | ||
| COM | doc_for_parentheses2 |
Parenthesizing a child according to its precedence. | ||
| COM | doc_for_precedence |
The precedence relation is a partial ordering between individual display forms, which is used in generating parentheses during display | ||
| COM | doc_for_precedence_classes |
How precedence classes are determined | ||
| COM | doc_for_precedence_derivation | How precedence is determined from the LAT objects and the precedence classes. ... | ||