Tags: mhuisi/lean4
Tags
feat: delaborator: use implicit lambdas where possible /cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's see if it is good enough in practice
feat: delaborator: use implicit lambdas where possible /cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's see if it is good enough in practice