strict spec using relation-algebra - Githubissues

Event-Structures / event-struct

Mechanized Theory of Event Structures

MIT License

16 stars 1 forks source link

strict spec using relation-algebra #68

Closed eupp closed 3 years ago

eupp commented 3 years ago

1) rename strict --> strictify (verb form, the name is debatable) 2) prove specification lemmas about strictify using relation-algebra

A minor related problem --- import of relation-algebra also brings in scope some definitions from vanilla Coq, which shadow ssrbool definitions (see lines 11-13). Any ideas on how to avoid this?