Commit 2023-06-20 12:36 ad017c0e

View on Github →

feat: add recall command (#5278)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Recall.lean

Created test/Recall.lean

added def foo