EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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.
The main match methods are:
1. Patterns may be nested, and a term is a pattern matching itself.
2. Edit slots are used as wild cards.
3. The explode form is used to specify patterns that match terms with non-homogeneous structure, such as various arities, opids, and variations on parameter structure and value. Edit slots in the exploded form that expect a sequence of structures actually match arbitrary sequences of such structures. doc for explode form
4. There are disjunction, conjunction, and negation expressions that can be used freely on any part of a pattern (including opid and binding variables in the exploded form).
<pattern>|<pattern>, <pattern>|&|<pattern> and |NOT|:<pattern>
are the forms.
5. There are expressions for matching module change of bound variables and for matching against variables (sometimes second-order). In these cases, no further recursive analysis is performed on the pattern.
|CBV|:<pattern> and |VARS|:<pattern> are the forms.
6. There is a *RECURSE* pattern that may be used within the pattern to match against a term recursively.
7. There is a pattern [string]:* which can match against any parameter type.
8. There are patterns [string]:substr, [string]:prefix, and [string]:suffix, for matching against substrings, prefixes, and suffixes of parameter values and opids.
9. As an abbreviation, the parameter matching forms mentioned in the previous couple of points will also match a term any of whose parameters or binding variables matches the pattern.
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
EditorDoc Sections Nuprl Doc