3 ms·
It's the size of the term. See this paper which proves the result for details: https://link.springer.com/chapter/10.1007/3-540-52590-4_50 https://link.springer.
by kachnuv_ocasek 3y ago
It's the size of the term. See this paper which proves the result for details: https://link.springer.com/chapter/10.1007/3-540-52590-4_50 https://link.springer.com/chapter/10.1007/3-540-52590-4_50
- mmoskal 3y agoMore specifically, time is almost linear with the size of the type, which can be doubly exponential compared to the program but people don't write such programs.