Documentation

Lean.Meta.Tactic.Subst

source
def Lean.Meta.substCore (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : optParam Bool false) (fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ }) (clearH : optParam Bool true) (tryToSkip : optParam Bool false) :
Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)
Instances For
    source
    def Lean.Meta.heqToEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (tryToClear : optParam Bool true) :
    Lean.MetaM (Lean.FVarId × Lean.MVarId)

    Given h : HEq α a α b in the given goal, produce a new goal where h : Eq α a b. If h is not of the give form, then just return (h, mvarId)

    Instances For
      source
      partial def Lean.Meta.subst (mvarId : Lean.MVarId) (h : Lean.FVarId) :
      Lean.MetaM Lean.MVarId
      source
      def Lean.Meta.subst.substEq (mvarId : Lean.MVarId) (h : Lean.FVarId) :
      Lean.MetaM Lean.MVarId

      Give h : Eq α a b, try to apply substCore

      Instances For
        source
        def Lean.Meta.subst.findEq (mvarId : Lean.MVarId) (h : Lean.FVarId) :
        Lean.MetaM Lean.MVarId

        Try to find an equation of the form heq : h = rhs or heq : lhs = h

        Instances For
          source
          def Lean.Meta.subst? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :
          Lean.MetaM (Option Lean.MVarId)
          Instances For
            source
            def Lean.Meta.substCore? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : optParam Bool false) (fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ }) (clearH : optParam Bool true) (tryToSkip : optParam Bool false) :
            Lean.MetaM (Option (Lean.Meta.FVarSubst × Lean.MVarId))
            Instances For
              source
              def Lean.Meta.trySubst (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :
              Lean.MetaM Lean.MVarId
              Instances For
                source
                def Lean.Meta.substSomeVar? (mvarId : Lean.MVarId) :
                Lean.MetaM (Option Lean.MVarId)
                Instances For
                  source
                  partial def Lean.Meta.substVars (mvarId : Lean.MVarId) :
                  Lean.MetaM Lean.MVarId