Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

RewTwo

Abstract

Licensed Foundation.Syntax.Predicate.Rew source excerpt selected for intended first-order pair and definition-elimination work.

Source-command excerpt selected from Foundation.Syntax.Predicate.Rew, lines 321-637, at Foundation revision 30a16ffa93d79d73ab4d02427fa00f50e039bf29. Historical consumer associations guided selection for intended first-order pair and definition-elimination work; current downstream use and necessity were not revalidated in this layer.

The Lean file retains selected upstream commands and their compiler companions. The immutable source map, modification notices, full Apache-2.0 license and retirement condition are in Library/ConceptDynamics/foundation2026firstorder.md.

The retained APIs are general term-rewriting machinery for formulas, rewriting operations, set operations, and proof and elaboration support. This excerpt does not itself establish a current pair interpretation and does not represent the full upstream module.

References