In Juvix Core we have a nameless representation by default, with names being introduced as an extension in HR (and HRAnn). By default, this unfortunately means that λx. t is represented as Lam t x. So it would be nice if the fields could be reordered.
A related idea is to have annotations which are products be split up in the patterns, e.g. being able to write (in Ann) (π f: s) (ρ e: t) as App π f s ρ e t instead of App f e (π, s, ρ, t)
In Juvix Core we have a nameless representation by default, with names being introduced as an extension in
HR(andHRAnn). By default, this unfortunately means thatλx. tis represented asLam t x. So it would be nice if the fields could be reordered.A related idea is to have annotations which are products be split up in the patterns, e.g. being able to write (in
Ann)(π f: s) (ρ e: t)asApp π f s ρ e tinstead ofApp f e (π, s, ρ, t)