lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
309 stars 25 forks source link

can scalar have a repr instance when ground fields do? #36

Closed alok closed 4 months ago

alok commented 4 months ago

missing repr is annoying

lecopivo commented 4 months ago

I don't understand, can you give mwe?

alok commented 4 months ago
class Scalar (R : outParam (Type _)) (K : semiOutParam (Type _)) extends RCLike K where
  -- used for specification
  toComplex : K → ℂ
  toReal    : R → ℝ
  ofReal    : ℝ → R
  ofComplex : ℂ → K -- If `K` model reals then this function should ignore the imaginary part

where if K (R too?) has Repr instance, so should Scalar

lecopivo commented 4 months ago

You need to be even more clearer. Scalar is a class, I don't understand why should it have Repr instance. Do you mean that Scalar should extend Repr R? That is probably bad idea as I don't think you can provide instance Repr Real