Add boolean facts and rewrite base

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

41 stars 24 forks source link

Add boolean facts and rewrite base #108

Closed DIJamner closed 11 months ago

DIJamner commented 11 months ago

This PR adds a set of lemmas, mostly rewrite rules collected into a rewrite base, about booleans. It's the start of migrating what is appropriate from Pyrosome's utils to this repo.