Documentation

Lean.Elab.Tactic.ShowTerm

source
def Lean.Elab.Tactic.ShowTerm.evalShowTerm :
Tactic
Equations
    Instances For
      source
      def Lean.Elab.Tactic.ShowTerm.elabShowTerm :
      Term.TermElab

      Implementation of show_term term elaborator.

      Equations
        Instances For