/usr/share/emacs/site-lisp/agda/agda2-abbrevs.el is in agda-mode 2.3.2.2-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | ;; agda2-abbrevs.el --- Default Agda abbrevs
;;; Commentary:
;;; Code:
;; Skeletons
(require 'skeleton)
(define-skeleton agda2-abbrevs-module
  "Inserts a module header template."
  nil
  "module " _ " where\n")
(define-skeleton agda2-abbrevs-data
  "Inserts a data template."
  nil
  "data " _ " : Set where\n")
(define-skeleton agda2-abbrevs-codata
  "Inserts a codata template."
  nil
  "codata " _ " : Set where\n")
(define-skeleton agda2-abbrevs-record
  "Inserts a record type template."
  nil
  "record " _ " : Set where\n"
  "  field\n")
(define-skeleton agda2-abbrevs-record-value
  "Inserts a record value template."
  nil
  "record {" _ "}")
(define-skeleton agda2-abbrevs-using
  "Inserts a using template."
  nil
  "using (" _ ")")
(define-skeleton agda2-abbrevs-hiding
  "Inserts a hiding template."
  nil
  "hiding (" _ ")")
(define-skeleton agda2-abbrevs-renaming
  "Inserts a renaming template."
  nil
  "renaming (" _ " to " _ ")")
(define-skeleton agda2-abbrevs-forall
  "Inserts a forall template."
  nil
  "∀ {" _ "} ")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Abbrevs
(defvar agda2-abbrevs-defaults '(
  ("m"   "" agda2-abbrevs-module)
  ("d"   "" agda2-abbrevs-data)
  ("c"   "" agda2-abbrevs-codata)
  ("re"  "" agda2-abbrevs-record)
  ("rec" "" agda2-abbrevs-record-value)
  ("u"   "" agda2-abbrevs-using)
  ("h"   "" agda2-abbrevs-hiding)
  ("r"   "" agda2-abbrevs-renaming)
  ("w"   "where\n")
  ("po"  "postulate")
  ("a"   "abstract\n")
  ("pr"  "private\n")
  ("pu"  "public")
  ("mu"  "mutual\n")
  ("f"   "" agda2-abbrevs-forall)
  ("oi"  "open import "))
  "Abbreviations defined by default in the Agda mode.")
(defcustom agda2-mode-abbrevs-use-defaults nil
  "If non-nil include the default Agda mode abbrevs in `agda2-mode-abbrev-table'.
The abbrevs are designed to be expanded explicitly, so users of `abbrev-mode'
probably do not want to include them.
Restart Emacs in order for this change to take effect."
  :group 'agda2
  :type '(choice (const :tag "Yes" t)
                 (const :tag "No" nil)))
(defvar agda2-mode-abbrev-table nil
  "Agda mode abbrev table.")
(define-abbrev-table
  'agda2-mode-abbrev-table
  (if agda2-mode-abbrevs-use-defaults
      (mapcar (lambda (abbrev)
                (append abbrev
                        (make-list (- 4 (length abbrev)) nil)
                        '((:system t))))
              agda2-abbrevs-defaults)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Administrative details
(provide 'agda2-abbrevs)
;;; agda2-abbrevs.el ends here
 |