Commit 2022-11-19 03:04 5c39c43d
View on Github →fix: use new coerce? API (#652)
https://github.com/leanprover/lean4/pull/1729 introduced a coercion API that is similar to the functions currently implemented by Mathlib.Tactic.Coe, so we can now directly use the core functions.
Apparently I also changed the mkCoe API, which broke the (↑) notation. This is also fixed by using the new functions.