LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.Meta

Auxiliary declarations for the Borel determinacy formalization.

def Parser.Attr.simp_lengths_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.simp_lengths : Lean.ParserDescr

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Parser.Attr.simp_fixing : Lean.ParserDescr

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Parser.Attr.simp_fixing_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.simp_isPosition_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.simp_isPosition : Lean.ParserDescr

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Lean.MVarId.getPropHyps (mvarId : MVarId) : MetaM (Array FVarId)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def simpLocationAtStar (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : Option Lean.Meta.Simp.Discharge := none) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def simpLocationAtStar.go (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : Option Lean.Meta.Simp.Discharge) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def simpAtStar : Lean.ParserDescr

Tactic support used by the Borel determinacy formalization.

Equations

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

def evalSimpAtStar : Lean.Elab.Tactic.Tactic

Auxiliary declaration for the Borel determinacy formalization.

Equations

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