- The new
setbindfunctions create binders that are alpha-equivalent “up to permutation”. For example, when quantifying over a list of type variables, their order really does not matter: . Unbound now lets you express this and takes it into account when testing alpha-equivalence.
- RepLib (and hence Unbound) now supports GADTs, as long as they do not contain any existential quantification.