search

DeepSpec / InteractionTrees

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

Indexed Coinduction #196

Open Lysxia opened 3 years ago

Lysxia commented 3 years ago

Reopening #189 which I closed by mistake

minkiminki commented 3 years ago

@gilhur and @alxest found that this indexed version of eutt does not work well. It is difficult to prove while f ~= while (Tau f) with the indexed one.