Zulip Chat Archive

Stream: general

Topic: nlinarith error message


Heather Macbeth (Jun 17 2020 at 23:28):

@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 (Jun 18 2020 at 08:06):

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 (Jun 18 2020 at 09:13):

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 (Jun 18 2020 at 09:26):

#3104


Last updated: Dec 20 2023 at 11:08 UTC