structure Batteries.Tactic.CollectOpaques.State : Type

Collects the result of a CollectOpaques query.

• visited : Lean.NameSet

  The set visited constants.

• opaques : Array Lean.Name

  The collected opaque defs.

@[reducible, inline]

abbrev Batteries.Tactic.CollectOpaques.M (α : Type) : Type

The monad used by CollectOpaques.

Equations

• Batteries.Tactic.CollectOpaques.M = ReaderT Lean.Environment (StateT Batteries.Tactic.CollectOpaques.State Lean.MetaM)

partial def Batteries.Tactic.CollectOpaques.collect (c : Lean.Name) : Batteries.Tactic.CollectOpaques.M Unit

Collect the results for a given constant.

def Batteries.Tactic.«command#printOpaques_» : Lean.ParserDescr

The command #print opaques X prints all opaque definitions that X depends on.

Opaque definitions include partial definitions and axioms. Only dependencies that occur in a computationally relevant context are listed, occurrences within proof terms are omitted. This is useful to determine whether and how a definition is possibly platform dependent, possibly partial, or possibly noncomputable.

The command #print opaques Std.HashMap.insert shows that Std.HashMap.insert depends on the opaque definitions: System.Platform.getNumBits and UInt64.toUSize. Thus Std.HashMap.insert may have different behavior when compiled on a 32 bit or 64 bit platform.

The command #print opaques Stream.forIn shows that Stream.forIn is possibly partial since it depends on the partial definition Stream.forIn.visit. Indeed, Stream.forIn may not terminate when the input stream is unbounded.

The command #print opaques Classical.choice shows that Classical.choice is itself an opaque definition: it is an axiom. However, #print opaques Classical.axiomOfChoice returns nothing since it is a proposition, hence not computationally relevant. (The command #print axioms does reveal that Classical.axiomOfChoice depends on the Classical.choice axiom.)

Equations

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