Simultaneous replacements broken in `Import ... with`

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax

https://abella-prover.org/

GNU General Public License v3.0

89 stars 18 forks source link

Closed chaudhuri closed 4 months ago

chaudhuri commented 7 months ago

a.thm

Type p, q prop.

b.thm

Type p, q prop.

Import "a" with p := q, q := p.

>>> Error: There are declared constants named q in import