Next:
The handling of variable
Up:
The implementation of the
Previous:
Examples of reasoning about
Implementing stratified abstraction in Watson
The most complex built-in functions of Watson are those which support stratified abstraction.
The handling of variable binding: de Bruijn levels and the formal definition of substitution
Abstraction and reduction by built-in tactics
Examples of the implementation of abstraction in Watson
The implementation of stratification in Watson: relative type and opacity
Examples of the implementation of stratification
Support for strongly cantorian domains
Examples of the implementation of strongly cantorian domains
Definitions in Watson
Fine points of matching: limited higher order matching and commutative matching
Special effects
Randall Holmes
2000-11-03
