Commits on Oct 19, 2024

1. chore: modify MonadStats to not extend parents multiple times …

   MonadStats was extending `MonadLiftT` twice, but the two parents were defeq. This was a hack to get around the fact that the parent instances were providing `MonadLiftT` instances rather than a `MonadLift` instance, breaking `MonadLiftT` inference.
   
   This changes it to *not* extend `MonadLiftT`, instead embedding it as a field, and then writing an explicit `MonadLift` instance.
   
   This is motivated by [lean4#5770](leanprover/lean4#5770), which will log warnings when structures extend parents multiple times.

   

   kmill committed Oct 19, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for cdea48a
   • Browse repository at this point

   Copy the full SHA

   cdea48a View commit details

   Browse the repository at this point in the history