mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 15:07:37 +03:00
d25db9e353
This completes the implementation of the examples in the paper "Applications of Applicative Proof Search" (Liam O'Connor, 2016). Unfortunately, the final example is an example of something that _can_ be expressed, but _cannot_ be model-checked by the approach in the paper. (Side note on `petersonsCorrect`: The paper mentions that it checks in ~3 minutes on a 2013 MacBook Pro. Assuming they mean "type-checks", this is roughly consistent with our observations of just short of 2 minutes. I doubt that they evaluated it, since an attempt at doing this on a reasonably modern server (Intel Xeon Gold 5220R, 502 GB of RAM) was killed after just over 3 hours, producing the following resource log: Command exited with non-zero status 255 Time: 11320.46s user, 35.12s system, 3h09m46s elapsed, 99%CPU Memory: 57644016 Kbytes RAM ) |
||
---|---|---|
.. | ||
base | ||
contrib | ||
linear | ||
network | ||
papers | ||
prelude | ||
test |