norm_num with int.fract

Stream: general

[Violeta Hernández]

Does norm_num support int.fract? I find this behavior odd:

-- works
example : int.fract (1 / 3 : ℚ) = 1 / 3 := by norm_num

-- fails
example : int.fract (-(2 / 3 : ℚ)) = 1 / 3 := by norm_num

[Violeta Hernández]

I think the first example might work just because it's simped down to 0 ≤ 1 / 3 ∧ 1 / 3 < 1.

[Mario Carneiro]

no