LP, the Larch Prover -- Name classes

A class is an expression that, when evaluated, produces a list of <name>s of facts.

Syntax

<class>          ::= <class-name> | <class-constant>
                        | <class-function> "(" <names> ")"
                        | contains-operator "(" <operator> ")"
                        | contains-variable "(" <variable> ")"
                        | copy "(" <class-name> ")"
<class-name>     ::= $ <simpleId>
<class-constant> ::= deduction-rules | formulas | induction-rules   
                       | operator-theories | rewrite-rules | active | passive 
                       | immune | nonimmune | ancestor-immune
<class-function> ::= ancestors | proper-ancestors | descendants
                       | proper-descendants | eval

Examples

$facts
contains-operator(+)
eval(* ~ $old)

Usage

The define-class command defines a <class-name> as an abbreviation for some <names>. Each <class>, other than ones beginning with copy or eval, also serves as an abbreviation for the names of facts matching a certain criterion. For example, contains-operator(+) describes the collection of all facts containing the operator +.

A <class-name> (or <class>) appearing in an argument to a command other than define-class is replaced by its definition (or evaluated) when the command is executed. Evaluation in the define-class command can be forced using one of the following operators:

copy($class)
Replaces the <class-name> $class by its current definition

eval(exp)
Replaces the <names> exp by an explicit list of the names of all facts in LP's logical system that match exp

See also