------------------------------------------------------------------------ -- The Agda standard library -- -- The reflexive transitive closures of McBride, Norell and Jansson -- -- This module is DEPRECATED. Please use the -- Relation.Binary.Closure.ReflexiveTransitive module directly. ------------------------------------------------------------------------ module Data.Star where open import Relation.Binary.Closure.ReflexiveTransitive public