This project is read-only.
1
Vote

Erroneous encoding of hypotheses involving primed variables

description

Sequents that have VARIABLE parameters, which occur primed in the hypotheses are translated inconsistently for the backends, making it impossible to apply them to prove anything. A minimal example is attached.

If you look at the input files produced for the different backends, the primed variable is called (something like) var' in some places and var_hash_prime in others.

file attachments

comments