Commit 2023-04-22 23:19 7fe00162
View on Github →feat: use more function coercions in apply_fun
(#3582)
When apply_fun f
is applied to the main goal, it creates the expression Function.Injective f
, which requires that f
be a function. Now apply_fun
will insert a function coercion here if needed. Furthermore, apply_fun
is now aware of Equiv.injective
.