The bug occurs when floating `cases_on` application in code of the form ``` let x := C.cases_on ... in t ``` and when the type of `t` depends on `x`. The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it. We fix the bug by replacing `x` with its value in the type. cc @kha |
||
|---|---|---|
| .. | ||
| init | ||
| leanpkg.path | ||
| library.md | ||
| Makefile.in | ||
| relative.py | ||