Simp attributes for the ZF realization machinery

This module registers the custom simp attributes used to drive the formula-realization and elementary-embedding automation in the rest of the development.

def Parser.Attr.realize_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.realize_simps : Lean.ParserDescr

Simp set for unfolding Formula.Realize of the generated ZF formulas.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.elementary_simps : Lean.ParserDescr

Simp set for pushing an elementary embedding through set-theoretic operations.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.elementary_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.elementary_simps_rev_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.elementary_simps_rev : Lean.ParserDescr

Reverse-direction simp set for elementary embeddings.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.toV_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.toV_simps : Lean.ParserDescr

Simp set for the toV map from a model into the von Neumann universe.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.toZFSet_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.toZFSet_simps : Lean.ParserDescr

Simp set for the toZFSet map from a model into ZFSet.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.formula_builder : Lean.ParserDescr

Simp set used while building first-order formulas from set-theoretic predicates.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.formula_builder_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.formula_builder_pre : Lean.ParserDescr

Pre-processing simp set used before building first-order formulas.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.formula_builder_pre_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.