This is a hackish module for hovering node information in the grind tactic state.

inductive Lean.Grind.NodeDef : Type

• unit : NodeDef

def Lean.Grind.node_def : Nat → {α : Sort u} → {a : α} → NodeDef

Equations

• Lean.Grind.node_def x✝ = Lean.Grind.NodeDef.unit

def Lean.Grind.nodeDefUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.NodeDefUnexpander : PrettyPrinter.Unexpander

Equations

• Lean.Grind.NodeDefUnexpander x✝ = pure (Lean.mkIdent (Lean.Name.mkSimple "NodeDef")).raw