Skip to content

Notation.Decimal

Martin Escardo 12th September 2024

This file provides an interface to implement automatic converscxion of
decimal literals to types other than just the natural numbers.

See https://agda.readthedocs.io/en/latest/language/literal-overloading.html


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

module Notation.Decimal where

open import MLTT.Universes
open import MLTT.NaturalNumbers

record Decimal {𝓀 π“₯ : Universe} (A : 𝓀 Μ‡ ) : 𝓀 βŠ” π“₯ ⁺ Μ‡ where
  field
    constraint : β„• β†’ π“₯ Μ‡
    fromβ„• : (n : β„•) {{_ : constraint n}} β†’ A

open Decimal {{...}} public using (fromβ„•)

{-# BUILTIN FROMNAT fromβ„• #-}
{-# DISPLAY Decimal.fromβ„• _ n = fromβ„• n #-}

record Negative {𝓀 π“₯ : Universe} (A : 𝓀 Μ‡ ) : 𝓀 βŠ” π“₯ ⁺ Μ‡ where
  field
    constraint : β„• β†’ π“₯ Μ‡
    fromNeg : (n : β„•) {{_ : constraint n}} β†’ A

open Negative {{...}} public using (fromNeg)

{-# BUILTIN FROMNEG fromNeg #-}
{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}

data No-Constraint : 𝓀₀ Μ‡ where
 no-constraint : No-Constraint

instance
 really-no-constraint : No-Constraint
 really-no-constraint = no-constraint

make-decimal-with-no-constraint
 : {A : 𝓀 Μ‡ }
 β†’ ((n : β„•)  {{_ : No-Constraint}} β†’ A)
 β†’ Decimal A
make-decimal-with-no-constraint f =
 record {
   constraint = Ξ» _ β†’ No-Constraint
 ; fromβ„• = f
 }

make-negative-with-no-constraint
 : {A : 𝓀 Μ‡ }
 β†’ ((n : β„•)  {{_ : No-Constraint}} β†’ A)
 β†’ Negative A
make-negative-with-no-constraint f =
 record {
   constraint = Ξ» _ β†’ No-Constraint
 ; fromNeg = f
 }


The natural place for this would be MLTT.NaturalNumbers, but then we
would get a circular dependency.


instance
 Decimal-β„•-to-β„• : Decimal β„•
 Decimal-β„•-to-β„• = make-decimal-with-no-constraint (Ξ» n β†’ n)