Environments shared by proof-carrying reification

def LeanCert.Tactic.Bridge.realEnvironment (values : List ℝ) (index : ℕ) : ℝ

Real environment used by proof-carrying reification. The unary case keeps the historical constant-environment convention; higher arities use zero beyond the supplied arguments.

Equations

• LeanCert.Tactic.Bridge.realEnvironment [value] index = value
• LeanCert.Tactic.Bridge.realEnvironment values index = values.getD index 0