Probably this should be conditional on the precedence of + (65) rather than "app" (1024)

I am struggling to make this happen, partly because I cannot think of a way to test this. I have updated everything else based on your feedback, thanks for that.

How would I go about defining the + precedence?

Maybe the easy way to test this would be to add a Repr for DualNumber (x + y*eps) at the same time, and check that DualNumber Complex has parentheses in the right place?

I will work on that, good suggestion.

I wrote this piece of code in Algebra/DualNumber.lean:

/-- Show DualNumber with values x and y as an "x + y*ε" string -/
instance instRepr [Repr R] : Repr (DualNumber R) where
  reprPrec f _p := repr f.fst ++ " + " ++ repr f.snd ++ "*ε"

I made Repr Complex print p, which was 0 for both cases (for a, b (both complex) in a + bε). This suggests to me that I am not getting sufficient information to conditionally print the brackets. I will for now opt to always print parentheses. I checked for Repr Rat as well, and that one does not add any outside brackets even though it is represented as a / b, which I'd presume should get parentheses if squared, for example.

Maybe I am missing something, but I tried finding other Repr's that handle conditionally adding brackets, and couldn't find anything.

I will also add parentheses for DualNumbers, to keep them consistent.

Let me know if there is a way, of course, but I do not see it.

The trick is that you should call reprPrec to pass in a p yourself

Bingo. I hardcoded the precedences for now, so if it is possible to use variables for those, let me know where I can find those and I will update those.

This is a great question; the best I could come up with was

elab:max "prec_of% " t:term : term => do
  let ⟨.node _ name _⟩ := t | throwErrorAt t "Cannot find syntax node"
  let p ← unsafe Lean.evalConst Lean.ParserDescr name
  let .trailingNode _ prec _ _ := p | throwErrorAt t "Cannot find precedence"
  return Lean.toExpr prec

#eval prec_of% _ * _