Commit 2023-02-02 19:41 a9f85121

View on Github →

feat: port qify (#2006) Easy adaptation of zify.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/Qify.lean

added theorem Mathlib.Tactic.Qify.int_cast_eq

added theorem Mathlib.Tactic.Qify.int_cast_le

added theorem Mathlib.Tactic.Qify.int_cast_lt

added theorem Mathlib.Tactic.Qify.int_cast_ne

Created Mathlib/Tactic/Qify/Attr.lean

Created test/Qify.lean