Documentation

Lean.Meta.PPGoal

opaque Lean.Meta.pp.auxDecls:

Lean.Option Bool

opaque Lean.Meta.pp.inaccessibleNames:

Lean.Option Bool

def Lean.Meta.withPPInaccessibleNamesImp {α : Type} (flag : Bool) (x : 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

structure Lean.Meta.ToHide.State:

Type

hiddenInaccessibleProp : Lean.FVarIdSet
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

@[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

Equations

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

def Lean.Meta.ToHide.unmark (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.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

Equations

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

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

Lean.Meta.ToHide.M Bool

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

Equations

Lean.Meta.ToHide.visitVisibleExpr e = do let a ← liftM (Lean.Meta.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)

Equations

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

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

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) (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.