Generating realization companion declarations

Build the formula, realization, and elementarity declarations registered by @[realize]. The expression representation and its correctness lemmas live in RealizeCore.

def BuildFormula.classIdents (typeLetter : String := "M") : BuildFormulaM (Array Lean.Ident)

The classIdents declaration.

Equations

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

def BuildFormula.varIdents (adjust? : Bool := false) (varLetter : String := "x") : BuildFormulaM (Array Lean.Ident)

The varIdents declaration.

Equations

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

def BuildFormula.hypothesisIdents (hypothesisLetter : String := "h") : BuildFormulaM (Array Lean.Ident)

The hypothesisIdents declaration.

Equations

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

def BuildFormula.identsBefore (i : ℕ) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM (Array Lean.Ident)

The identsBefore declaration.

Equations

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

def BuildFormula.allIdentsWithHypotheses (typeLetter : String := "M") (varLetter : String := "x") (hypothesisLetter : String := "h") : BuildFormulaM (Array Lean.Ident)

The allIdentsWithHypotheses declaration.

Equations

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

def BuildFormula.classParamBinders (typeLetter : String := "M") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The classParamBinders declaration.

Equations

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

def BuildFormula.mkBinders (adjust? : Bool := false) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The mkBinders declaration.

Equations

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

def BuildFormula.mkTermApp (x : Lean.Term) (xs : Array Lean.Term) : BuildFormulaM Lean.Term

The mkTermApp declaration.

Equations

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

def BuildFormula.mkParam (i : ℕ) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM Lean.Term

The mkParam declaration.

Equations

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

def BuildFormula.mkBindersWithHypotheses (typeLetter : String := "M") (varLetter : String := "x") (hypothesisLetter : String := "h") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The mkBindersWithHypotheses declaration.

Equations

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

def BuildFormula.mkIdent' (name : Lean.Name) : Lean.Ident

The mkIdent' declaration.

Equations

• BuildFormula.mkIdent' name = Lean.mkIdent (`_root_ ++ name)

def BuildFormula.buildFunction (funcName : Lean.Name) : BuildFormulaM Unit

The buildFunction declaration.

Equations

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

def BuildFormula.realizedTerm (typeLetter : String := "M") : BuildFormulaM Lean.Term

The realizedTerm declaration.

Equations

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

def BuildFormula.buildRealizeIff (thmName : Lean.Name) : BuildFormulaM Unit

The buildRealizeIff declaration.

Equations

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

def BuildFormula.buildInstFormulaToFunction (instName : Lean.Name) : BuildFormulaM Unit

The buildInstFormulaToFunction declaration.

Equations

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

def BuildFormula.mkVarVec (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM Lean.Term

The mkVarVec declaration.

Equations

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

def BuildFormula.buildToRealize (toRealizeName : Lean.Name) : BuildFormulaM Unit

The buildToRealize declaration.

Equations

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

def BuildFormula.buildElementarity (elementarityName : Lean.Name) : BuildFormulaM Unit

The buildElementarity declaration.

Equations

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

def BuildFormula.runIfNotFound (names : List Lean.Name) (f : Lean.Name → BuildFormulaM Unit) : BuildFormulaM Unit

The runIfNotFound declaration.

Equations

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

def BuildFormula.realizeAttrAdd (attrDeclName : Lean.Name) : Lean.AttrM Unit

Build all the Formula.Realize companion declarations for the decl attrDeclName tagged with @[realize].

Equations

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