Meta results regarding sorry and pseudo attributions

Some of the code here is adapted from from the file: Lean.Util.CollectAxioms copyright (c) 2020 Microsoft Corporation. Authored by Leonardo de Moura.

structure PhysLean.CollectSorry.State : Type

A structure used for collecting names of results dependent on the sorryAx axiom and the Lean.ofReduceBool axiom.

• visited : Lean.NameSet

  The names which have already been visited as part of the state.

• containsSorry : Lean.NameSet

  The names which depend on the sorryAx axiom.

• containsOfReduceBool : Lean.NameSet

  The names which depend on the Lean.ofReduceBool axiom.

@[reducible, inline]

abbrev PhysLean.CollectSorry.M (α : Type) : Type

A monad used for collecting names of results dependent on the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

• PhysLean.CollectSorry.M = ReaderT Lean.Environment (StateM PhysLean.CollectSorry.State)

partial def PhysLean.CollectSorry.collect (c : Lean.Name) (parents : Lean.NameSet) : M Unit

Given a c : Name updating the monad M based on which results which c uses depend on the sorryAx axiom and the Lean.ofReduceBool axiom.

def PhysLean.CollectSorry.allSorryPseudo (c : Array Lean.Name) : M Unit

Given a c : Array Name updating the monad M based on which results depend on the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

• PhysLean.CollectSorry.allSorryPseudo c = Array.forM (fun (x : Lean.Name) => PhysLean.CollectSorry.collect x ∅) c

def PhysLean.collectSorryPseudo (c : Array Lean.Name) : Lean.CoreM (Array Lean.Name × Array Lean.Name)

Given a c : Array Name the names of all results used to defined the results in c with the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

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

def PhysLean.allWithSorryPseudo : Lean.CoreM (Array Lean.Name × Array Lean.Name)

The axioms of a constant.

Equations

• PhysLean.allWithSorryPseudo = do let __do_lift ← PhysLean.allUserConsts let x ← PhysLean.collectSorryPseudo (Array.map (fun (c : Lean.ConstantInfo) => c.name) __do_lift) pure x

unsafe def PhysLean.allSorryfulAttributed : Lean.CoreM (Array Lean.Name)

All names which are attributed sorryful.

Equations

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

unsafe def PhysLean.allPseudoAttributed : Lean.CoreM (Array Lean.Name)

All names which are attributed pseudo.

Equations

• PhysLean.allPseudoAttributed = do let env ← Lean.getEnv let pseudoInfos : Array PseudoInfo := pseudoExtension.getState env pure (Array.map (fun (info : PseudoInfo) => info.name) pseudoInfos)

unsafe def PhysLean.sorryfulPseudoTest : Lean.MetaM Unit

Checks whether all results attributed sorryful depend on the ```sorryAx` axiom and vice versa.

Equations

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