Yicheng Tao
Results
3
comments of
Yicheng Tao
@PhotonQuantum
Is there any progress? Just fail to interact with theorem in mathlib using v4.14.0.
> For what it's worth my understanding is that auto-implicits are a useful feature for experienced Lean users but they are an absolute tripping hazard for new users... Thanks for...