------------------------------------------------------------------------
-- Some instances related to the natrec-star operator
------------------------------------------------------------------------

module Graded.Modality.Natrec-star-instances {a} {M : Set a} where

open import Graded.Modality M

open Has-star ⦃ … ⦄ public