• 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-abbreviation

Convert a time zone to an abbreviation string.

Signature

(time-zone-abbreviation zone daylight-p) → *

Arguments

zone — Guard (rationalp zone).

This will map certain time zone values to abbreviations. There are many time zone values which correspond to multiple time zones. The choice of mapped time zone is therefore largely arbitrary. Time zone values which are not mapped are instead rendered as a UTC offset. See time-zone-to-utc-string.

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

Definitions and Theorems

Function: time-zone-abbreviation

(defun time-zone-abbreviation (zone daylight-p)
  (declare (xargs :guard (rationalp zone)))
  (declare (xargs :split-types t)
           (type rational zone))
  (let ((__function__ 'time-zone-abbreviation))
    (declare (ignorable __function__))
    (case zone
      (-14 "LINT")
      (-12 (if daylight-p "NZDT" "NZST"))
      (-11 "SBT")
      (-10 (if daylight-p "AEDT" "AEST"))
      (-19/2 (if daylight-p "ACDT" "ACST"))
      (-9 "JST")
      (-8 (if daylight-p "CST China" "AWST"))
      (-7 "WIB")
      (-13/2 "MMT")
      (-6 "BST")
      (-23/4 "NPT")
      (-11/2 "IST")
      (-5 "PKT")
      (-9/2 "AFT")
      (-4 "GST")
      (-7/2 "IRST")
      (-3 "MSK")
      (-2 (if daylight-p "EEST" "EET"))
      (-1 (if daylight-p "CEST" "CET"))
      (0 "GMT")
      (1 "AZOT")
      (2 "GST")
      (3 "BRT")
      (7/2 (if daylight-p "NDT" "NST"))
      (4 (if daylight-p "ADT" "AST"))
      (5 (if daylight-p "EDT" "EST"))
      (6 (if daylight-p "CDT" "CST"))
      (7 (if daylight-p "MDT" "MST"))
      (8 (if daylight-p "PDT" "PST"))
      (9 (if daylight-p "AKDT" "AKST"))
      (10 "HST")
      (11 "SST")
      (12 "BIT")
      (otherwise (time-zone-to-utc-string zone)))))