------------------------------------------------------------------------
-- The Agda standard library
--
-- Printf
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Text.Printf where
open import Data.String.Base using (String; fromChar; concat)
open import Function.Base using (id)
import Data.Integer.Show as ℤ
import Data.Float.Base as Float
import Data.Nat.Show as ℕ
open import Text.Format as Format hiding (Error)
open import Text.Printf.Generic
printfSpec : PrintfSpec formatSpec String
printfSpec .PrintfSpec.renderArg ℕArg = ℕ.show
printfSpec .PrintfSpec.renderArg ℤArg = ℤ.show
printfSpec .PrintfSpec.renderArg FloatArg = Float.show
printfSpec .PrintfSpec.renderArg CharArg = fromChar
printfSpec .PrintfSpec.renderArg StringArg = id
printfSpec .PrintfSpec.renderStr = id
module Printf = Type formatSpec
open Printf public hiding (map)
open Render printfSpec public renaming (printf to gprintf)
printf : (fmt : String) → Printf (lexer fmt) String
printf fmt = Printf.map (lexer fmt) concat (gprintf fmt)
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