------------------------------------------------------------------------ -- The Agda standard library -- -- Metrics with ℕ as the codomain of the metric function ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Function.Metric.Nat where open import Function.Metric.Nat.Core public open import Function.Metric.Nat.Definitions public open import Function.Metric.Nat.Structures public open import Function.Metric.Nat.Bundles public