computable operations for rational numbers

Stream: Is there code for X?

[Adam Topaz]

Is there any way to make the following work?

example : (0 : ℚ) + 1 = 1 := dec_trivial

[Adam Topaz]

I would like to do some (formally verified) linear algebra over the rationals, but I don't want to work too hard...

[Gabriel Ebner]

(deleted)

[Yakov Pechersky]

Does by norm_num work?

[Adam Topaz]

I guess so, but let me try a more realistic example...

[Adam Topaz]

Ah nice,

example : ![(0 : ℚ),1,2] + ![1,2,3] = ![1,3,5] := by norm_num

works just fine!

[Adam Topaz]

But it's not perfect...

I was dumb.... this works:

example : (1/2 : ℚ) • ![(0 : ℚ),1,0] = ![0,1/2,0] := by norm_num

[Eric Rodriguez]

yeah, you were using nat-div