search

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

Reduce for lists #342

Closed hulsemohit closed 1 year ago

hulsemohit commented 1 year ago

I've implemented a reduce operation for lists. I've also added elaboration and notations for reduce. This PR also includes the new type_eq_dec (no longer relying on Scheme Equality) and the associated changes to the elaborator we discussed during the last meeting.