coinductive version of always - Githubissues

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

41 stars 24 forks source link

coinductive version of always #113

Closed andres-erbsen closed 7 months ago

andres-erbsen commented 7 months ago

please fast-forward for https://github.com/mit-plv/fiat-crypto/pull/1846