This transformation tries to push the type abstractions (big lambdas /\ x : Type .) to the front of terms, before any term abstractions (small lambdas \ x : Int .)
For example,
/\ a : Type . \ x : a . /\ b : Type . \ y : b . ...
is transformed to
/\ a : Type . /\ b : Type . \ x : a . \ y : b . ...
This makes it easier for later transformations to apply on type abstractions. In fact, it's common to just bail out on non-prenex types in other transformations, because those cases are quite rare and difficult to handle (usually involving some impredicative types.)
This transformation tries to push the type abstractions (big lambdas
/\ x : Type .) to the front of terms, before any term abstractions (small lambdas\ x : Int .)For example,
is transformed to
This makes it easier for later transformations to apply on type abstractions. In fact, it's common to just bail out on non-prenex types in other transformations, because those cases are quite rare and difficult to handle (usually involving some impredicative types.)