Documentation

Lean.Meta.Tactic.Delta

source
def Lean.Meta.delta? (e : Lean.Expr) (p : optParam (Lake.Name → Bool) fun (x : Lake.Name) => true) :
Lean.CoreM (Option Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.deltaExpand (e : Lean.Expr) (p : Lake.Name → Bool) :
    Lean.CoreM Lean.Expr

    Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.MVarId.deltaTarget (mvarId : Lean.MVarId) (p : Lake.Name → Bool) :
      Lean.MetaM Lean.MVarId

      Delta expand declarations that satisfy p at mvarId type.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[deprecated Lean.MVarId.deltaTarget]
        def Lean.Meta.deltaTarget (mvarId : Lean.MVarId) (p : Lake.Name → Bool) :
        Lean.MetaM Lean.MVarId
        Equations
        Instances For
          source
          def Lean.MVarId.deltaLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (p : Lake.Name → Bool) :
          Lean.MetaM Lean.MVarId

          Delta expand declarations that satisfy p at fvarId type.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[deprecated Lean.MVarId.deltaLocalDecl]
            def Lean.Meta.deltaLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (p : Lake.Name → Bool) :
            Lean.MetaM Lean.MVarId
            Equations
            Instances For