Documentation

Lean.Elab.Tactic.Delta

source
def Lean.Elab.Tactic.deltaLocalDecl (declNames : Array Name) (fvarId : FVarId) :
TacticM Unit
Equations
    Instances For
      source
      def Lean.Elab.Tactic.deltaTarget (declNames : Array Name) :
      TacticM Unit
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.evalDelta :
          Tactic

          "delta " ident+ (location)?

          Equations
            Instances For