Jan Mas Rovira

Mutually recursive blocks are sometimes wrong

1

E.g. ``` module Example; type Fun := mkFun (T -> T); type T := mkT; ``` is incorrectly translated (with `juvix dev internal pretty Example.juvix`) to ``` module MutualIssue; mutual...

E.g. it should be possible to write ``` isMember {A} (testEq : A → A → Bool) (element : A) (list : List A) : Bool := case list of...

Consider this example: ``` module example; import Library.Delta as Delta; module Resource; module Delta; end; open Delta; -- ambiguity error between imported Delta and local module Delta. end; ``` There...

In the following example we get an error at the last `return` because we are unable to find a monad instance for `M`. We should detect `Monad M` because we...

Applicative do notation is similar to monadic do notation with a few differences: 1. Only pure expressions and bind statements are allowed. I.e., there are no let statements. 3. Last...