module Prim.Literals where
Primitive: Overloaded literalsπ
We define the records Number, Negative and String to allow overloading of the numeric literals.
record Number {a} (A : Type a) : Type (lsuc a) where field Constraint : Nat β Type a fromNat : β n β {{_ : Constraint n}} β A open Number {{...}} public using (fromNat) record Negative {a} (A : Type a) : Type (lsuc a) where field Constraint : Nat β Type a fromNeg : β n β {{_ : Constraint n}} β A open Negative {{...}} public using (fromNeg) {-# BUILTIN FROMNAT fromNat #-} {-# DISPLAY Number.fromNat _ n = fromNat n #-} {-# BUILTIN FROMNEG fromNeg #-} {-# DISPLAY Negative.fromNeg _ n = fromNeg n #-} postulate String : Type {-# BUILTIN STRING String #-} record IsString {a} (A : Type a) : Type (lsuc a) where field Constraint : String β Type a fromString : (s : String) {{_ : Constraint s}} β A open IsString {{...}} public using (fromString) {-# BUILTIN FROMSTRING fromString #-} {-# DISPLAY Number.fromNat _ n = fromNat n #-} {-# DISPLAY IsString.fromString _ s = fromString s #-} {-# DISPLAY Negative.fromNeg _ n = fromNeg n #-} instance Number-Nat : Number Nat Number-Nat .Number.Constraint _ = β€ Number-Nat .Number.fromNat n = n IsString-String : IsString String IsString-String .IsString.Constraint _ = β€ IsString-String .IsString.fromString s = s