    ------------------------------------------------------------------------
    -- 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)