------------------------------------------------------------------------ -- Some instances related to the nr function and the natrec-star -- operator ------------------------------------------------------------------------ module Graded.Modality.Nr-instances {a} {M : Set a} where open import Graded.Modality M open Has-nr ⦃ … ⦄ public open Has-star ⦃ … ⦄ public