Re: [isabelle] linarith_split_limit_exceeded (current value is 9)
Hi Angeliki, you have a number of options for modifying this limit:
At the top level of a theory file:
declare [[linarith_split_limit = 15]]
At the top level of a proof:
note [[linarith_split_limit = 15]]
Before an individual proof step:
using [[linarith_split_limit = 15]]
What I don’t know was how high you can take this limit before things fall apart.
> On 28 May 2020, at 12:15, Dr A. Koutsoukou-Argyraki <ak2110 at cam.ac.uk> wrote:
> In my formalisation I'm using various very simple algebraic calculations
> as I do everything step by step
> ( adding up factors, expanding/ getting rid of - outside parentheses, showing equality of algebraic expressions etc etc.. )that I
> would expect would be solved by linarith or simp or auto.
> Very often, when I call Sledgehammer or try0 I keep getting
> "Proof found"
> and then repeatedly the message :
> linarith_split_limit_exceeded (current value is 9)"
> I can see this issue has been discussed before but I'm not sure how I could get rid of this problem.
> Is there some setting/ macro/plugin I could change perhaps?
> Many thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and