Alok Singh

some incremental elab has been added, maybe good time to revisit this?

working on adding lawful functor to array, did it for list. my main difficulty is that proving stuff for list is easier because of the inductive def, but array doesn't...

i'd be happy to tackle this, though a bit of guidance would be very appreciated.

see you on zulip then

``` class Scalar (R : outParam (Type _)) (K : semiOutParam (Type _)) extends RCLike K where -- used for specification toComplex : K → ℂ toReal : R →...

```lean /-- A doc string -/ def foo := 1 @[inherit_doc foo] def bar := 2 -- Hover over 'bar' ABOVE rather than the one below #eval bar ``` Hovering...