Commit 2023-11-15 21:24 e194c756
View on Github →perf(FunLike.Basic): beta reduce CoeFun.coe (#7905)
This eliminates (fun a ↦ β) α in the type when applying a FunLike.
perf(FunLike.Basic): beta reduce CoeFun.coe (#7905)
This eliminates (fun a ↦ β) α in the type when applying a FunLike.