mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-04 19:05:25 +03:00
211de419bb
This was a slight difference from Blodwen that wasn't accounted for - there might be lets in the nested environment, so when building the expanded application type, make sure we go under them |
||
|---|---|---|
| .. | ||
| expected | ||
| input | ||
| LetCase.idr | ||
| run | ||
| Stuff.idr | ||