vellvm / ctrees

An itree-like data-structure to additionally support internal non-determinism
MIT License
14 stars 3 forks source link

Make embed_eq pass #18

Closed elefthei closed 2 years ago

YaZko commented 2 years ago

Hey Lef, thanks for the PR! I need to look at this closely, I had this proof clean and complete in master, it should be straight up transferable here too, I didn't know it was currently broken.

The full merge from master to this branch that I promised you earlier this week has been delayed sorry, but I'll get to it asap --- I hope before Monday, if I'm quick enough at finishing preparing a talk.