Documentation

Init.Grind.PP

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

source
inductive Lean.Grind.NodeDef :
Type
Instances For
    source
    def Lean.Grind.node_def :
    Nat → {α : Sort u} → {a : α} → NodeDef
    Equations
      Instances For
        source
        def Lean.Grind.nodeDefUnexpander :
        PrettyPrinter.Unexpander
        Equations
          Instances For
            source
            def Lean.Grind.NodeDefUnexpander :
            PrettyPrinter.Unexpander
            Equations
              Instances For