opaque Lean.Meta.pp.auxDecls : Lean.Option Bool

opaque Lean.Meta.pp.inaccessibleNames : Lean.Option Bool

opaque Lean.Meta.pp.showLetValues : Lean.Option Bool

def Lean.Meta.withPPInaccessibleNamesImp {α : Type} (flag : Bool) (x : Lean.MetaM α) : Lean.MetaM α

Equations

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

def Lean.Meta.withPPInaccessibleNames {m : Type → Type u_1} {α : Type} [inst : MonadControlT Lean.MetaM m] [inst : Monad m] (x : m α) (flag : optParam Bool true) : m α

Equations

• Lean.Meta.withPPInaccessibleNames x flag = Lean.Meta.mapMetaM (fun {α} => Lean.Meta.withPPInaccessibleNamesImp flag) x

def Lean.Meta.withPPShowLetValuesImp {α : Type} (flag : Bool) (x : Lean.MetaM α) : Lean.MetaM α

Equations

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

def Lean.Meta.withPPShowLetValues {m : Type → Type u_1} {α : Type} [inst : MonadControlT Lean.MetaM m] [inst : Monad m] (x : m α) (flag : optParam Bool true) : m α

Equations

• Lean.Meta.withPPShowLetValues x flag = Lean.Meta.mapMetaM (fun {α} => Lean.Meta.withPPShowLetValuesImp flag) x

def Lean.Meta.withPPForTacticGoal {m : Type → Type u_1} {α : Type} [inst : MonadControlT Lean.MetaM m] [inst : Monad m] (x : m α) : m α

Set pretty-printing options (pp.showLetValues = true and pp.inaccessibleNames = true) for visualizing goals.

Equations

• Lean.Meta.withPPForTacticGoal x = Lean.Meta.withPPShowLetValues (Lean.Meta.withPPInaccessibleNames x)

structure Lean.Meta.ToHide.State : Type

• FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types

  hiddenInaccessibleProp : Lean.FVarIdSet

• FVarIds with inaccessible names, but not in hiddenInaccessibleProp

  hiddenInaccessible : Lean.FVarIdSet
• modified : Bool

structure Lean.Meta.ToHide.Context : Type

• If true we make a declaration "visible" if it has visible backward dependencies. Remark: recall that for the Prop case, the declaration is moved to hiddenInaccessibleProp

  backwardDeps : Bool
• goalTarget : Lean.Expr
• showLetValues : Bool

@[inline]

abbrev Lean.Meta.ToHide.M (α : Type) : Type

Equations

• Lean.Meta.ToHide.M = ReaderT Lean.Meta.ToHide.Context (StateRefT' IO.RealWorld Lean.Meta.ToHide.State Lean.MetaM)

def Lean.Meta.ToHide.isMarked (fvarId : Lean.FVarId) : Lean.Meta.ToHide.M Bool

Return true if fvarId is marked as an hidden inaccessible or inaccessible proposition

Equations

• Lean.Meta.ToHide.isMarked fvarId = do let s ← get pure (Lean.RBTree.contains s.hiddenInaccessible fvarId || Lean.RBTree.contains s.hiddenInaccessibleProp fvarId)

def Lean.Meta.ToHide.unmark (fvarId : Lean.FVarId) : Lean.Meta.ToHide.M Unit

If fvarId isMarked, then unmark it.

Equations

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

def Lean.Meta.ToHide.moveToHiddeProp (fvarId : Lean.FVarId) : Lean.Meta.ToHide.M Unit

Equations

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

def Lean.Meta.ToHide.hasVisibleDep (localDecl : Lean.LocalDecl) : Lean.Meta.ToHide.M Bool

Return true if the given local declaration has a "visible dependency", that is, it contains a free variable that is hiddenInaccessible

Recall that hiddenInaccessibleProps are visible, only their names are hidden

Equations

• Lean.Meta.ToHide.hasVisibleDep localDecl = do let s ← get Lean.Meta.ToHide.findDeps localDecl fun a => !Lean.RBTree.contains s.hiddenInaccessible a

def Lean.Meta.ToHide.hasInaccessibleNameDep (localDecl : Lean.LocalDecl) : Lean.Meta.ToHide.M Bool

Return true if the given local declaration has a "nonvisible dependency", that is, it contains a free variable that is hiddenInaccessible or hiddenInaccessibleProp

Equations

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

def Lean.Meta.ToHide.visitVisibleExpr (e : Lean.Expr) : Lean.Meta.ToHide.M Unit

If e is visible, then any inaccessible in e marked as hidden should be unmarked.

Equations

• Lean.Meta.ToHide.visitVisibleExpr e = do let a ← Lean.instantiateMVars e Lean.MonadCacheT.run (Lean.Meta.ToHide.visitVisibleExpr.visit a)

partial def Lean.Meta.ToHide.visitVisibleExpr.visit (e : Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit Lean.Meta.ToHide.M Unit

def Lean.Meta.ToHide.fixpointStep : Lean.Meta.ToHide.M Unit

Equations

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

partial def Lean.Meta.ToHide.fixpoint : Lean.Meta.ToHide.M Unit

def Lean.Meta.ToHide.collect (goalTarget : Lean.Expr) : Lean.MetaM (Lean.FVarIdSet × Lean.FVarIdSet)

If pp.inaccessibleNames == false, then collect two sets of FVarIds : hiddenInaccessible and hiddenInaccessibleProp 1- hiddenInaccessible contains FVarIds of free variables with inaccessible names that a) are not propositions or b) are propositions containing "visible" names. 2- hiddenInaccessibleProp contains FVarIds of free variables with inaccessible names that are propositions containing "visible" names. Both sets do not contain FVarIds that contain visible backward or forward dependencies. The goalTarget counts as a forward dependency.

We say a name is visible if it is a free variable with FVarId not in hiddenInaccessible nor hiddenInaccessibleProp

For propositions in hiddenInaccessibleProp, we show only their types when displaying a goal.

Remark: when pp.inaccessibleNames == true, we still compute hiddenInaccessibleProp to prevent the goal from being littered with irrelevant names.

Equations

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

def Lean.Meta.getGoalPrefix (mvarDecl : Lean.MetavarDecl) : String

Equations

• Lean.Meta.getGoalPrefix mvarDecl = if Option.isSome (Lean.isLHSGoal? mvarDecl.type) = true then "| " else "⊢ "

def Lean.Meta.ppGoal (mvarId : Lean.MVarId) : Lean.MetaM Lean.Format

Equations

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

def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Lean.Name) (type? : Option Lean.Expr) (fmt : Lean.Format) : Lean.MetaM Lean.Format

Equations

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

def Lean.Meta.ppGoal.ppVars (indent : Int) (showLetValues : Bool) (hiddenProp : Lean.FVarIdSet) (varNames : List Lean.Name) (prevType? : Option Lean.Expr) (fmt : Lean.Format) (localDecl : Lean.LocalDecl) : Lean.MetaM (List Lean.Name × Option Lean.Expr × Lean.Format)

Equations

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