Stream: new members
Chris M (Jun 08 2020 at 06:00):
I'm unsure how exactly I can predict when Lean will be able to infer an implicit argument, i.e. when I can use f _ instead of f y. I could just use trial and error, but is there a simple, principled idea of when it is possible or not for Lean to infer something?
Last updated: May 15 2021 at 22:14 UTC