mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Try assumption when checking if purified hyp already derivable #397

Closed vfukala closed 9 months ago

vfukala commented 9 months ago

Instead of just running xlia, checking if the purified version of a hyp can already be derived now also splits all ands and tries the assumption tactic.