|
|
|
|
|
|
by pron
3314 days ago
|
|
|
If you have support for coinductive data types then you are Turing complete. Proof: you can simulate a Turing machine. However, Coq's term language is not Turing complete, meaning that every syntactic element in Coq evaluates to a terminating computation. |
|
|