------------------------------------------------------------------------
-- The Agda standard library
--
-- Metrics with ℚ as the codomain of the metric function
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Function.Metric.Rational where

open import Function.Metric.Rational.Core public
open import Function.Metric.Rational.Definitions public
open import Function.Metric.Rational.Structures public
open import Function.Metric.Rational.Bundles public