Open shmish111 opened 4 years ago
This bit of the parser is responsible: once we have seen let
we commit to
either a block of let-binders or a block of local definitions. We could instead
allow interleavings of the two.
https://github.com/edwinb/Idris2/blob/19426ecd141f93c34268a53ed09b5e48e64ba73b/src/Idris/Parser.idr#L553-L570
I think it's reasonable to allow interleavings of the two different let
forms.
Fighting the type errors but I have good hope I'll have something soon.
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
Steps to Reproduce
Check
Expected Behavior
Type checks fine
Observed Behavior
It can be 'fixed' by having a separate let block for things with type annotations and things without. If this is expected behaviour then: