• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
      • Get-decoded-time$
        • Time-zone-abbreviation
        • Time-zone-to-utc-string
      • Argv
      • Copy
      • Catpath
      • Ls
      • Universal-time
      • Tempfile
      • Basename
      • Dirname
      • Copy!
      • Ls-files
      • Mkdir
      • Date
      • Rmtree
      • Lisp-version
      • Lisp-type
      • Ls-subdirs
      • Getpid
      • Dirnames
      • Basenames
      • Basename!
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Ls!
      • Catpaths
      • Mkdir!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Get-decoded-time$

Time-zone-to-utc-string

Convert a time zone to a UTC offset string.

Signature

(time-zone-to-utc-string zone) → *

Arguments

zone — Guard (rationalp zone).

See get-decoded-time$ for a description of time zone values.

Definitions and Theorems

Function: time-zone-to-utc-string

(defun time-zone-to-utc-string (zone)
  (declare (xargs :guard (rationalp zone)))
  (declare (xargs :split-types t)
           (type rational zone))
  (let ((__function__ 'time-zone-to-utc-string))
    (declare (ignorable __function__))
    (let* ((sign (if (<= zone 0) "+" "-"))
           (total-minutes (abs (floor (* zone 60) 1)))
           (hours (floor total-minutes 60))
           (minutes (mod total-minutes 60)))
      (cat "UTC" sign (natstr (floor hours 10))
           (natstr (mod hours 10))
           ":" (natstr (floor minutes 10))
           (natstr (mod minutes 10))))))