Def Tactic.NormCast.getSimpArgs

Modification history

2022-09-06 13:11

Mathlib/Tactic/NormCast/Ext.lean

chore: update lean + std4 09-05 (#401)

Deleted Tactic.NormCast.getSimpArgs View on Github →

2022-02-24 13:15

Mathlib/Tactic/NormCast/Ext.lean

feat: `norm_cast` (#191)

Added Tactic.NormCast.getSimpArgs View on Github →