syntax list(X) = X* -- if |X*| < 2^32
syntax name = char* -- if |$utf8(name)| < 2^32
which are needed to represent the spec faithfully. For this purpose, IL Notation types can now have premises, too.
With that, EL range types are now also properly lowered into Notation types instead of plain nat/int.
This required a couple of minor extensions to the IL and its reduction rules in order to express projection from Notation types (UnmixE) and a few generalisations to pattern matching.
This PR enables the definition of types like
which are needed to represent the spec faithfully. For this purpose, IL Notation types can now have premises, too.
With that, EL range types are now also properly lowered into Notation types instead of plain nat/int.
This required a couple of minor extensions to the IL and its reduction rules in order to express projection from Notation types (UnmixE) and a few generalisations to pattern matching.