Arithmetic operations with a precision parameter

Stream: mathlib4

[Geoffrey Irving]

Say I have a type T with bunch of arithmetic operations (Mul, Add, Div, Pow, etc.) but where each takes an extra precision : Nat parameter. Is there a nice way of representing things so that one can specify the overall precision of an expression with a bunch of arithmetic operators, and use normal arithmetic notation within the expression?

[Geoffrey Irving]

That is, I want to be able to write something like withPrec p (x * y + z) and have it expand to (x.mul y p).add z p where T.mul : T -> T -> (precision : Nat) -> T and similar.

[Daniel Weber]

You can define a type synonym

def Prec (prec : Nat) := T

And then define instances on it which use the prec, and finally define

def withPrec (prec : Nat) (val : Prec prec) : T := val

[Daniel Weber]

You might also need to define a coercion from T to Prec n

[Geoffrey Irving]

Nice, that's a lot simpler than the kind of type class implicit thing I was imagining.

[Eric Wieser]

Another option is to have an elab that expands to letI := myAddWithPrec p; letI := myMulWithPrec p; $arg

[Eric Wieser]

(where the two names are instances)