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
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
Instances For
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
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
Instances For
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
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
Instances For
Modify mvarId target type using f.
Instances For
Instances For
Modify mvarId target type left-hand-side using f.
Throw an error if target type is not an equality.