Documentation

Lean.Meta.Tactic.Replace

Convert the given goal Ctx |- target into Ctx |- targetNew using an equality proof eqProof : target = targetNew. It assumes eqProof has type target = targetNew

Instances For
    @[deprecated Lean.MVarId.replaceTargetEq]
    Instances For

      Convert the given goal Ctx |- target into Ctx |- targetNew. It assumes the goals are definitionally equal. We use the proof term

      @id target mvarNew
      

      to create a checkpoint.

      Instances For
        @[deprecated Lean.MVarId.replaceTargetDefEq]
        Instances For
          @[inline, reducible]

          Replace type of the local declaration with id fvarId with one with the same user-facing name, but with type typeNew. This method assumes eqProof is a proof that type of fvarId is equal to typeNew. This tactic actually adds a new declaration and (try to) clear the old one. If the old one cannot be cleared, then at least its user-facing name becomes inaccessible. Remark: the new declaration is added immediately after fvarId. typeNew must be well-formed at fvarId, but eqProof may contain variables declared after fvarId.

          Instances For
            @[inline, reducible, deprecated Lean.MVarId.replaceLocalDecl]
            Instances For

              Replace the type of fvarId at mvarId with typeNew. Remark: this method assumes that typeNew is definitionally equal to the current type of fvarId.

              Instances For
                @[deprecated Lean.MVarId.replaceLocalDeclDefEq]
                Instances For
                  def Lean.MVarId.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :

                  Replace the target type of mvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to the current target type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to the current target type.

                  Instances For
                    @[deprecated Lean.MVarId.change]
                    def Lean.Meta.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                    Instances For

                      Replace the type of the free variable fvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to fvarId type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to fvarId type.

                      Instances For
                        @[deprecated Lean.MVarId.changeLocalDecl]
                        def Lean.Meta.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) :
                        Instances For

                          Modify mvarId target type using f.

                          Instances For
                            @[deprecated Lean.Meta.modifyTarget]
                            Instances For

                              Modify mvarId target type left-hand-side using f. Throw an error if target type is not an equality.

                              Instances For
                                @[deprecated Lean.MVarId.modifyTargetEqLHS]
                                Instances For