1ea4bdb9cd
closes #341 This is another instance of a compiler bug. It is in the code that is still written in C/C++. We need to infer types in the compiler, and we reused the kernel type checker for this. However, the compiler performs transformations that may produce type incorrect terms. This happens in code that makes heavy use of dependent types (like the new test). This is just a workaround for this particular instance of the problem. The definitive solution will only happen when we replace this part of the compiler with Lean code, and implement a custom `inferType` method for the compiler. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| leanpkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||