Subject: Refiner

Keywords: ::Rules

Title: Rule interpreter args

--------------------------------------------------

Rule args occur as:
  - Patterns in rule definitions.
     * term-sig indicates some intent as to use.  
  - ML expressions for building rule instances.
      * primitive types for diff args
  - terms in rule instances 
      * converted from ml args.
 
Patterns in rule definitions:
  - assumption-index{n}
  - bound_id(1)
      x.T -> T[b/x] where b is bound by match in rule
      should be an error for x to be otherwise instantiated
  - parameter{l}
  - <term>
  - variable{v} : meant to introduce a fresh variable name


⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t
              RICH:t

⋅

Home