deriving Repr for functions

Stream: lean4

[Yuri de Wit]

Although (think) I understand why, it is still a bit disappointing that we can't automatically derive Repr when a type has function parameters, for instance.

Unless Repr is supposed to also support reading/parsing the generated representation, could the default deriving generate a dummy #function of something along these lines? At least we wouldnt throw the baby with the bath water.

Consider the following example:

inductive Value
| mk (data: Float)
      (prev : Array Value /- := .none -/)
      (op: Option Op := .none)
      (label : Option String := "")
      (grad : Float := 0.0)
      (backward : Unit -> Unit := fun () => ())
deriving Repr

And the error:

failed to synthesize instance
Repr (Unit → Unit)

[Yuri de Wit]

Nevermind:

instance : Repr (Unit -> Unit) where
  reprPrec
    | _, _  => "#function"

In any case, the question about making it a default still holds, no?

[James Gallicchio]

I would suggest _ : F -> G with some macro magic to print the types out, but +1 to adding it as a default instance to Std