------------------------------------------------------------------------
-- 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
open Is-factoring-nr ⦃ … ⦄ public