awalterschulze / regex-reexamined-coq

Apache License 2.0
21 stars 7 forks source link

change definition of and to be property based #159

Closed awalterschulze closed 3 years ago

awalterschulze commented 3 years ago

Review, but DO NOT MERGE This requires https://github.com/awalterschulze/regex-reexamined-coq/pull/158 to merge this. Let me worry about doing it in the right order.

Fixes https://github.com/awalterschulze/regex-reexamined-coq/issues/154

and_lang is redefined as P /\ Q and not defined in terms of or_lang nor_lang is redefined as s \notin P /\ s \notin Q and not defined in terms of or_lang

awalterschulze commented 3 years ago

Discussed offline: merging now and will post review