Def Mathlib.Tactic.pushFVarAliasInfo

Modification history

2024-07-15 21:28

Mathlib/Tactic/Basic.lean

chore(Tactic): reduce use of autoImplicit, part 3 (#14770)

Modified Mathlib.Tactic.pushFVarAliasInfo View on Github →

2023-03-29 23:55

Mathlib/Tactic/Basic.lean

fix: alias FVarIds for `change` and `clear_value` (#2937) …

Added Mathlib.Tactic.pushFVarAliasInfo View on Github →