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.

Larry

> On 28 May 2020, at 12:15, Dr A. Koutsoukou-Argyraki <ak2110 at cam.ac.uk> wrote:
> 
> Hello,
> 
> 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,
> Angeliki
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.