Def Linarith.ExprMultiMap.insert

Modification history

2024-07-16 20:24

Mathlib/Tactic/Linarith/Frontend.lean

chore(Tactic): reduce autoImplicit, part 4 (#14805) …

Modified Linarith.ExprMultiMap.insert View on Github →

2023-01-25 11:55

Mathlib/Tactic/Linarith/Frontend.lean

fix: instantiate mvars before pattern matching on Type (#1775) …

Added Linarith.ExprMultiMap.insert View on Github →