The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 11/05/2015 02:40, Katherine Ye wrote:
> Any help would be appreciated.

It seems that you're lacking the definition of eqLinProp as an
equivalence relation...

> Other suggestions about ways to represent the environment, which is a
> set that can contain the same element multiple times, are also
> welcome. (I considered Ensembles and ListSet, but they were missing
> things. Maybe lists with permutations?)

I made a proof of completeness of phase semantics once, using lists up
to permutations. It is here.

https://github.com/ppedrot/ll-coq

PMP

Attachment: signature.asc
Description: OpenPGP digital signature