search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

Fixing the definition of mrec_fix. #171

Closed Mbodin closed 4 years ago

Mbodin commented 4 years ago

Fixes #170.

Lysxia commented 4 years ago

Thanks a lot for this fix!

I wonder whether it would be possible to have a solution that survives simplification, but I couldn't figure it out; I'll keep track of that in another issue.