Failure to assign distinct internal names to variables

[rappatoni]

In the following, A2 causes an error while A1 is fine error.txt

import mitm http://mathhub.info/MitM/Foundation ❚

theory test : mitm:?Logic =
    testdomain : type ❘ #T  ❙
    A1: ⊦ ∃[m:T] (m ≐ m) ∨ ∃[n:T] (n ≐ n) ❙
    A2: ⊦ ∃[n:T] (n ≐ n) ∨ ∃[n:T] (n ≐ n) ❙
❚

It appears that mmt fails to assign fresh internal variables n/r within the scope of each existential quantifier?

[florian-rabe]

@kohlhase @Jazzpirate

This was due to a so far unspecified aspect of the behavior: Can an unknown term depend on a shadowed variable? I've now pushed a version (to devel branch) that answers this question negatively.

In the above example, the unknown type of the second equality can now depend on

• m and n in A1
• only the second n in A2 That works in the above example.

However, there are reasonable cases, where the unknown does depend on a shadowed variable. Example: the unknown argument of equality in [x: type, c: x, x: type] c = c. These did not work correctly before and do not now either.

Can you check your example again?

[florian-rabe]

To avoid confusion, note that MMT parses the second quantifier to be in the scope of the first.

[rappatoni]

I tried. I am now getting invalid unit errors for both A1 and A2: error2.txt.

Dennis thinks this is probably an unrelated issue stemming from recent changes to the solver?

[florian-rabe]

At that time, a lot was changing.

I've ironed out must bugs by now. So maybe try again.