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.

Estimated changes