Def Mathlib.Tactic.Rewrites.RewriteResult.computeRfl

Modification history

2024-05-02 13:42

Mathlib/Tactic/Rewrites.lean

chore: move to v4.8.0-rc1 (#12548) …

Deleted Mathlib.Tactic.Rewrites.RewriteResult.computeRfl View on Github →

2023-06-05 07:16

Mathlib/Tactic/Rewrites.lean

fix: rewrites doesn't fail when trying an unimported lemma (#4537) …

Added Mathlib.Tactic.Rewrites.RewriteResult.computeRfl View on Github →