Assignment operator in forall_inst args

@hbarbosa, @hjsc and I discussed and decided that the arguments of the forall_inst rule should be printed as equalities and not as assignments:

assigned to @hjsc

assigned to @hjsc

changed the description

Update:

My original proposal was a misunderstanding. We do still want to change this though. Haniel proposed a list of options to move forward with this. After discussion seems like the following seems best.

use a list of the terms instantiating the quantifier. For example:

(step i (cl (not (forall ((x T) (y T)) (P x y))) (P t1 t2)) :rule forall_inst :args (t1 t2))

The downside is that solvers must both instantiate the quantifier fully and pass the terms in the right order.

However, it is not clear how hard it is to change veriT to do so.

mentioned in merge request !7 (merged)

closed

reopened

So if I am not mistaken this is now in the standard, and implemented by veriT.

added todo-Carcara todo-Isabelle todo-cvc5 labels

It is also done in cvc5 and in Carcara (in the versions I'm maintaining to sync-up. To be merged into the main repos soon).

removed todo-Carcara label

removed todo-cvc5 label

Awesome, then I'll move forward with supporting it in Isabelle

removed todo-Isabelle label

I think this has been addressed in all the needed places so we can close it?

closed