projects / coinductive-monad.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 68eb561) | patch
add example showing why we cannot simply extract the witness from TerminatesWith...
authoradam <adam@megacz.com>
Sun, 28 Oct 2007 22:24:07 +0000 (22:24 +0000)
committeradam <adam@megacz.com>
Sun, 28 Oct 2007 22:24:07 +0000 (22:24 +0000)
commit9ce6a85d86cdc3a5bba1f5c3cd153cdc046f10b9
tree02b36a978dbf99f7344b3769bcd2eec91e7d8f79tree | snapshot
parent68eb561f71dd052a346319cd1b92dd077cb1c8bbcommit | diff
add example showing why we cannot simply extract the witness from TerminatesWith to get a trivial eval

darcs-hash:20071028222407-5007d-35f02a37ae798d87d4dc41385d07f6a687c1b2d3.gz
Computation/Eval.v diff | blob | history
Code accompanying the paper __A Coinductive Monad for Prop-Bounded Recursion__