Def Tactic.NormCast.registerCoercion

Modification history

2022-09-06 13:11

Mathlib/Tactic/NormCast/CoeExt.lean

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

Deleted Tactic.NormCast.registerCoercion View on Github →

2022-02-24 13:15

Mathlib/Tactic/NormCast/CoeExt.lean

feat: `norm_cast` (#191)

Added Tactic.NormCast.registerCoercion View on Github →