------------------------------------------------------------------------ -- Restrictions on usage derivations ------------------------------------------------------------------------ module Graded.Usage.Restrictions {a} (M : Set a) where open import Tools.Level -- Restrictions on usage derivations. record Usage-restrictions : Set (lsuc a) where no-eta-equality field -- The prodrec constructor's quantities have to satisfy this -- predicate. Prodrec-allowed : (r p q : M) → Set a