Simplify euttG - Githubissues

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 simplified the definition of euttG as follows:

from gpaco2 ... (transU rH \2/ transD rL) (transU rH \2/ transD rL \2/ transD gL)
to gpaco2 ... (transU rH \2/ rL) gL

YaZko commented 5 years ago

Ah those look great, thanks Gil!