------------------------------------------------------------------------
-- The Agda standard library
--
-- Format strings for Printf and Scanf
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Text.Format where
open import Data.Maybe.Base
open import Text.Format.Generic
-- Formatted types
open import Data.Char.Base using (Char)
open import Data.Integer.Base using (ℤ)
open import Data.Float.Base using (Float)
open import Data.Nat.Base using (ℕ)
open import Data.String.Base using (String)
------------------------------------------------------------------------
-- Basic types
data ArgChunk : Set where
ℕArg ℤArg FloatArg CharArg StringArg : ArgChunk
------------------------------------------------------------------------
-- Semantics
ArgType : (fmt : ArgChunk) → Set
ArgType ℕArg = ℕ
ArgType ℤArg = ℤ
ArgType FloatArg = Float
ArgType CharArg = Char
ArgType StringArg = String
lexArg : Char → Maybe ArgChunk
lexArg 'd' = just ℤArg
lexArg 'i' = just ℤArg
lexArg 'u' = just ℕArg
lexArg 'f' = just FloatArg
lexArg 'c' = just CharArg
lexArg 's' = just StringArg
lexArg _ = nothing
formatSpec : FormatSpec
formatSpec .FormatSpec.ArgChunk = ArgChunk
formatSpec .FormatSpec.ArgType = ArgType
formatSpec .FormatSpec.lexArg = lexArg
open Format formatSpec public
pattern `ℕ = Arg ℕArg
pattern `ℤ = Arg ℤArg
pattern `Float = Arg FloatArg
pattern `Char = Arg CharArg
pattern `String = Arg StringArg
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4