Generalize "eq" to "RR" in the equational theory.

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

199 stars 50 forks source link

Closed gilhur closed 5 years ago

gilhur commented 5 years ago

I generalized the equality theory as requested by Steve.

Zdancewic commented 5 years ago

Thanks, Gil! We will merge this pull request as part of the AsmOptimization branch.