As uncovered by PR #2389 it seems that the preferred style ```agda private variable a : Level ``` isn't actually documented.