redefining operators

Stream: new members

[pblpbl]

Hello, is it possible to redefine existing operators? Currently I'm trying to make / always return a real number when called on Nat using
def div (a b : ℝ) : ℝ := a / b infix:70 "/" => div

but I'm getting ambiguous, possible interpretations when trying to use it.

[Kyle Miller]

You could override the interpretation of a pre-existing notation with a macro, like

macro_rules | `($a / $b) => `((HDiv.hDiv ($a : ℝ) ($b : ℝ) : ℝ))

(untested)

[Kyle Miller]

This is better than using your div too since all theorems are in terms of HDiv.hDiv

[Edward van de Meent]

i think the preferable method would be to define a different notation, for example something like "/r"

[Michal Wallace (tangentstorm)]

÷?