38d9a7c063
@Kha Could you please take a look at this repro? When I use the compiler, ``` ./run.sh usizeBug.lean ``` I get the expected answer: `2`. When I use the interpreter, ``` ../../bin/lean --run usizeBug.lean ``` I get `1`. I found the problem today, and managed to isolate the problem to this small repro. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| playground | ||
| plugin | ||