nlinarith error message

Stream: general

[Heather Macbeth]

@Rob Lewis Today I tried the new nlinarith and received a strange error message: "app_builder_exception, more information can be obtained using command set_option trace.app_builder true". Here are two simplified examples:

import algebra.group
import tactic.linarith

variables {E : Type*} [add_group E]

example (f : ℤ → E) (h : 0 = f 0) : 1 ≤ 2 := by nlinarith
example (a : E) (h : a = a) : 1 ≤ 2  := by nlinarith

Any ideas?

[Rob Lewis]

Yeah, I see the issue. I was lazy and tried to use a shortcut for equality hypotheses that clearly doesn't work. Not too hard to fix.

[Rob Lewis]

Oh, no, that's not it. My shortcut works fine. It's just an error handling thing. An add_group isn't enough for linarith so it should ignore the hypotheses over E instead of failing.

[Rob Lewis]

#3104