------------------------------------------------------------------------ -- The Agda standard library -- -- Some properties related to Data.Star -- -- This module is DEPRECATED. Please use the -- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties -- module directly. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Star.Properties where open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties public