Change the def of "eutt" - Githubissues

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

204 stars 51 forks source link

Change the def of "eutt" #71

Closed gilhur closed 5 years ago

gilhur commented 5 years ago

"eutt" provides very strong reasoning principles.
Simplify the proofs a lot and kill all the admits.