Re: [Why3-club] Instantiating a value on a term from a cloned theory

2014-09-30 Thread Guillaume Melquiond
On 30/09/2014 15:36, K. Siaulys wrote: Hello everybody, I hope this is a right place to ask a question. I am also very new to Why3, therefore I apologise if the question is trivial. Basically, I have two theories - one that should hold a declared but undefined integer term t, and a second one t

[Why3-club] Instantiating a value on a term from a cloned theory

2014-09-30 Thread K. Siaulys
Hello everybody, I hope this is a right place to ask a question. I am also very new to Why3, therefore I apologise if the question is trivial. Basically, I have two theories - one that should hold a declared but undefined integer term t, and a second one that should clone the first one and i