Def Linarith.partitionByType

Modification history

2023-01-25 11:55

Mathlib/Tactic/Linarith/Frontend.lean

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

Modified Linarith.partitionByType View on Github →

2022-11-28 22:26

Mathlib/Tactic/Linarith/Frontend.lean

feat: port linarith (#526) …

Added Linarith.partitionByType View on Github →