|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
;; This file:
;; http://angg.twu.net/.emacs.agda.html
;; http://angg.twu.net/.emacs.agda
;; (find-angg ".emacs.agda")
;; Author: Eduardo Ochs <eduardoochs@gmail.com>
;;
;; Loaded from: (find-angg ".emacs" "agda")
;; «.find-agdatype» (to "find-agdatype")
;; «.user-manual» (to "user-manual")
;; «.plfa-chapters» (to "plfa-chapters")
;; «.plfa1» (to "plfa1")
;; «.plfa2» (to "plfa2")
;; «.plfa3» (to "plfa3")
;; «.plfa4» (to "plfa4")
;; «.plfa5» (to "plfa5")
;; «.plfa6» (to "plfa6")
;; «.plfa7» (to "plfa7")
;; «.plfa8» (to "plfa8")
;; «.plfa9» (to "plfa9")
;; «.recordstutorial» (to "recordstutorial")
;; «.wadler-leibniz» (to "wadler-leibniz")
;; «.wadler-smbf» (to "wadler-smbf")
;; «.agdamodeel» (to "agdamodeel")
;; «.glyphs» (to "glyphs")
;; «.C-c-C-SPC» (to "C-c-C-SPC")
;; «.hott» (to "hott")
;; «.eec-agdalatex» (to "eec-agdalatex")
(defun eejump-554 () (find-angg ".emacs.agda"))
;; (find-es "agda" "agda-inst-clai")
(code-c-d "agdagit" "~/usrc/agda/")
(code-c-d "agdaprim" "~/usrc/agda/src/data/lib/prim/")
;; (find-agdagitfile "")
;; «find-agdatype» (to ".find-agdatype")
;; (find-angg "AGDA/find-agdatype.el")
(load "~/AGDA/find-agdatype.el")
;; «user-manual» (to ".user-manual")
;; (find-es "agda" "agda-inst-bum")
;; (find-LATEX "catsem-ab.bib" "bib-AgdaUserManual")
(code-pdf-page "agdausermanual" "~/usrc/agda/doc/user-manual.pdf")
(code-pdf-text "agdausermanual" "~/usrc/agda/doc/user-manual.pdf" 4)
(code-c-d "agdausermanual" "~/usrc/agda/doc/user-manual/_build/html/")
(code-c-d "agdausermanualsrc" "~/usrc/agda/doc/user-manual/")
;; (find-agdausermanualsrcfile "")
;; (find-agdausermanualpage)
;; (find-agdausermanualtext)
;; (find-agdausermanualpage (+ 4 3) "1 Overview")
;; (find-agdausermanualpage (+ 4 5) "2 Getting Started")
;; (find-agdausermanualpage (+ 4 5) "2.1 What is Agda?")
;; (find-agdausermanualpage (+ 4 7) "2.2 Prerequisites")
;; (find-agdausermanualpage (+ 4 7) "2.3 Installation")
;; (find-agdausermanualpage (+ 4 11) "2.4 `Hello world' in Agda")
;; (find-agdausermanualpage (+ 4 12) "2.5 Quick Guide to Editing, Type Checking and Compiling Agda Code")
;; (find-agdausermanualpage (+ 4 14) "2.6 A List of Tutorials")
;; (find-agdausermanualpage (+ 4 17) "3 Language Reference")
;; (find-agdausermanualpage (+ 4 17) "3.1 Abstract definitions")
;; (find-agdausermanualpage (+ 4 20) "3.2 Built-ins")
;; (find-agdausermanualpage (+ 4 31) "3.3 Coinduction")
;; (find-agdausermanualpage (+ 4 34) "3.4 Copatterns")
;; (find-agdausermanualpage (+ 4 37) "3.5 Core language")
;; (find-agdausermanualpage (+ 4 37) "3.6 Cubical")
;; (find-agdausermanualpage (+ 4 50) "3.7 Cumulativity")
;; (find-agdausermanualpage (+ 4 51) "3.8 Data Types")
;; (find-agdausermanualpage (+ 4 54) "3.9 Flat Modality")
;; (find-agdausermanualpage (+ 4 55) "3.10 Foreign Function Interface")
;; (find-agdausermanualpage (+ 4 61) "3.11 Function Definitions")
;; (find-agdausermanualpage (+ 4 64) "3.12 Function Types")
;; (find-agdausermanualpage (+ 4 65) "3.13 Generalization of Declared Variables")
;; (find-agdausermanualpage (+ 4 70) "3.14 Implicit Arguments")
;; (find-agdausermanualpage (+ 4 72) "3.15 Instance Arguments")
;; (find-agdausermanualpage (+ 4 78) "3.16 Irrelevance")
;; (find-agdausermanualpage (+ 4 83) "3.17 Lambda Abstraction")
;; (find-agdausermanualpage (+ 4 85) "3.18 Local Definitions: let and where")
;; (find-agdausermanualpage (+ 4 89) "3.19 Lexical Structure")
;; (find-agdausermanualpage (+ 4 93) "3.20 Literal Overloading")
;; (find-agdausermanualpage (+ 4 95) "3.21 Mixfix Operators")
;; (find-agdausermanualpage (+ 4 97) "3.22 Module System")
;; (find-agdausermanualpage (+ 4 102) "3.23 Mutual Recursion")
;; (find-agdausermanualpage (+ 4 104) "3.24 Pattern Synonyms")
;; (find-agdausermanualpage (+ 4 105) "3.25 Positivity Checking")
;; (find-agdausermanualpage (+ 4 107) "3.26 Postulates")
;; (find-agdausermanualpage (+ 4 108) "3.27 Pragmas")
;; (find-agdausermanualpage (+ 4 111) "3.28 Prop")
;; (find-agdausermanualpage (+ 4 113) "3.29 Record Types")
;; (find-agdausermanualpage (+ 4 120) "3.30 Reflection")
;; (find-agdausermanualpage (+ 4 130) "3.31 Rewriting")
;; (find-agdausermanualpage (+ 4 132) "3.32 Run-time Irrelevance")
;; (find-agdausermanualpage (+ 4 134) "3.33 Safe Agda")
;; (find-agdausermanualpage (+ 4 135) "3.34 Sized Types")
;; (find-agdausermanualpage (+ 4 138) "3.35 Syntactic Sugar")
;; (find-agdausermanualpage (+ 4 143) "3.36 Syntax Declarations")
;; (find-agdausermanualpage (+ 4 143) "3.37 Telescopes")
;; (find-agdausermanualpage (+ 4 144) "3.38 Termination Checking")
;; (find-agdausermanualpage (+ 4 146) "3.39 Universe Levels")
;; (find-agdausermanualpage (+ 4 150) "3.40 With-Abstraction")
;; (find-agdausermanualpage (+ 4 162) "3.41 Without K")
;; (find-agdausermanualpage (+ 4 165) "4 Tools")
;; (find-agdausermanualpage (+ 4 165) "4.1 Automatic Proof Search (Auto)")
;; (find-agdausermanualpage (+ 4 168) "4.2 Command-line options")
;; (find-agdausermanualpage (+ 4 178) "4.3 Compilers")
;; (find-agdausermanualpage (+ 4 180) "4.4 Emacs Mode")
;; (find-agdausermanualpage (+ 4 186) "4.5 Literate Programming")
;; (find-agdausermanualpage (+ 4 188) "4.6 Generating HTML")
;; (find-agdausermanualpage (+ 4 188) "4.7 Generating LaTeX")
;; (find-agdausermanualpage (+ 4 205) "4.8 Library Management")
;; (find-agdausermanualpage (+ 4 208) "4.9 Performance debugging")
;; (find-agdausermanualpage (+ 4 209) "4.10 Search Definitions in Scope")
;; (find-agdausermanualpage (+ 4 211) "5 Contribute")
;; (find-agdausermanualpage (+ 4 211) "5.1 Documentation")
;; (find-agdausermanualpage (+ 4 215) "6 The Agda Team and License")
;; (find-agdausermanualpage (+ 4 217) "7 Indices and tables")
;; (find-agdausermanualpage (+ 4 219) "Bibliography")
;; (find-agdausermanualpage (+ 4 221) "Index")
;; (find-agdausermanualfile "")
;; (find-agdausermanualfile "" "index.html")
;; «plfa-chapters» (to ".plfa-chapters")
;; (find-es "agda" "plfa-chapters-prince")
;; (find-LATEX "catsem-ab.bib" "bib-WadlerPLFA")
;;
(code-c-d "plfa" "~/usrc/plfa/")
(code-pdf-page "plfa1" "~/PLFA/1._GettingStarted.pdf")
(code-pdf-text "plfa1" "~/PLFA/1._GettingStarted.pdf")
(code-pdf-page "plfa2" "~/PLFA/2._Naturals.pdf")
(code-pdf-text "plfa2" "~/PLFA/2._Naturals.pdf")
(code-pdf-page "plfa3" "~/PLFA/3._Induction.pdf")
(code-pdf-text "plfa3" "~/PLFA/3._Induction.pdf")
(code-pdf-page "plfa4" "~/PLFA/4._Relations.pdf")
(code-pdf-text "plfa4" "~/PLFA/4._Relations.pdf")
(code-pdf-page "plfa5" "~/PLFA/5._Equality.pdf")
(code-pdf-text "plfa5" "~/PLFA/5._Equality.pdf")
(code-pdf-page "plfa6" "~/PLFA/6._Isomorphism.pdf")
(code-pdf-text "plfa6" "~/PLFA/6._Isomorphism.pdf")
(code-pdf-page "plfa7" "~/PLFA/7._Connectives.pdf")
(code-pdf-text "plfa7" "~/PLFA/7._Connectives.pdf")
(code-pdf-page "plfa8" "~/PLFA/8._Negation.pdf")
(code-pdf-text "plfa8" "~/PLFA/8._Negation.pdf")
(code-pdf-page "plfa9" "~/PLFA/9._Quantifiers.pdf")
(code-pdf-text "plfa9" "~/PLFA/9._Quantifiers.pdf")
(code-pdf-page "plfa10" "~/PLFA/10._Decidable.pdf")
(code-pdf-text "plfa10" "~/PLFA/10._Decidable.pdf")
(code-pdf-page "plfa11" "~/PLFA/11._Lists.pdf")
(code-pdf-text "plfa11" "~/PLFA/11._Lists.pdf")
(code-c-d "plfastdlib" "~/usrc/plfa/standard-library/src/")
;; (find-plfastdlibfile "")
(code-c-d "agdacats" "~/usrc/agda-categories/")
(code-c-d "agdacatsc" "~/usrc/agda-categories/src/Categories/")
;; (find-agdacatsfile "")
;; (find-agdacatscfile "")
;; (find-plfafile "")
;; «plfa1» (to ".plfa1")
;; (find-plfafile "README.md")
;; (find-plfa1page)
;; (find-plfa1text)
;; (find-plfa1page 3 "Agda standard library")
;; (find-plfa1text 3 "Agda standard library")
;; (find-plfa1page 7 "Using agda-mode in Emacs")
;; (find-plfa1text 7 "Using agda-mode in Emacs")
;; (find-plfa1page 7 "C-c C-l")
;; (find-plfa1text 7 "C-c C-l")
;; (find-plfa1page 8 "C-c C-c : case split")
;; (find-plfa1text 8 "C-c C-c : case split")
;; (find-plfa1page 9 "M-x quail-show-key")
;; (find-plfa1text 9 "M-x quail-show-key")
;; «plfa2» (to ".plfa2")
;; (find-plfafile "src/plfa/part1/Naturals.lagda.md")
;; (find-plfa2page)
;; (find-plfa2text)
;; (find-plfa2page 6 "Imports")
;; (find-plfa2text 6 "Imports")
;; (find-plfa2page 17 "Writing definitions interactively")
;; (find-plfa2text 17 "Writing definitions interactively")
;; «plfa3» (to ".plfa3")
;; (find-plfafile "src/plfa/part1/Induction.lagda.md")
;; (find-plfa3page)
;; (find-plfa3text)
;; (find-plfa3page 1 "module plfa.part1.Induction")
;; (find-plfa3text 1 "module plfa.part1.Induction")
;; (find-plfa3page 5 "Our first proof: associativity")
;; (find-plfa3text 5 "Our first proof: associativity")
;; (find-plfa3page 10 "Our second proof: commutativity")
;; (find-plfa3text 10 "Our second proof: commutativity")
;; (find-plfa3page 16 "section notation" "Richard Bird")
;; (find-plfa3text 16 "section notation" "Richard Bird")
;; (find-plfa3page 17 "Associativity with rewrite")
;; (find-plfa3text 17 "Associativity with rewrite")
;; (find-plfa3page 18 "Commutativity with rewrite")
;; (find-plfa3text 18 "Commutativity with rewrite")
;; (find-plfa3page 19 "Building proofs interactively")
;; (find-plfa3text 19 "Building proofs interactively")
;; (find-plfa3page 23 "Definitions similar to those")
;; (find-plfa3text 23 "Definitions similar to those")
;; «plfa4» (to ".plfa4")
;; (find-plfafile "src/plfa/part1/Relations.lagda.md")
;; (find-plfa4page)
;; (find-plfa4text)
;; (find-plfa4page 3 "Implicit arguments")
;; (find-plfa4text 3 "Implicit arguments")
;; (find-plfa4page 5 "Properties of ordering relations")
;; (find-plfa4text 5 "Properties of ordering relations")
;; «plfa5» (to ".plfa5")
;; (find-plfafile "src/plfa/part1/Equality.lagda.md")
;; (find-plfa5page)
;; (find-plfa5text)
;; (find-plfa5page 4 "Congruence and substitution")
;; (find-plfa5text 4 "Congruence and substitution")
;; (find-plfa5page 5 "Chains of equations")
;; (find-plfa5text 5 "Chains of equations")
;; (find-plfa5page 6 "module -Reasoning {A : Set} where")
;; (find-plfa5text 6 "module -Reasoning {A : Set} where")
;; (find-plfa5page 8 "we postulate")
;; (find-plfa5text 8 "we postulate")
;; (find-plfa5page 9 "equivalent to its simplified term")
;; (find-plfa5text 9 "equivalent to its simplified term")
;; (find-plfa5page 9 "same simplified form")
;; (find-plfa5text 9 "same simplified form")
;; (find-plfa5page 10 "Rewriting")
;; (find-plfa5text 10 "Rewriting")
;; (find-plfa5page 12 "Multiple rewrites")
;; (find-plfa5text 12 "Multiple rewrites")
;; «plfa6» (to ".plfa6")
;; (find-plfafile "src/plfa/part1/Isomorphism.lagda.md")
;; (find-plfa6page)
;; (find-plfa6text)
;; «plfa7» (to ".plfa7")
;; (find-es "agda" "connectives")
;; (find-plfafile "src/plfa/part1/Connectives.lagda.md")
;; (find-plfa7page)
;; (find-plfa7text)
;; (find-plfa7page 3 "binds less tightly")
;; (find-plfa7text 3 "binds less tightly")
;; «plfa8» (to ".plfa8")
;; (find-plfafile "src/plfa/part1/Negation.lagda.md")
;; (find-plfa8page)
;; (find-plfa8text)
;; «plfa9» (to ".plfa9")
;; (find-plfafile "src/plfa/part1/Quantifiers.lagda.md")
;; (find-plfa9page)
;; (find-plfa9text)
;; (find-plfa10page)
;; (find-plfa10text)
;; (find-plfa11page)
;; (find-plfa11text)
;; «recordstutorial» (to ".recordstutorial")
;; (find-es "agda" "records")
(code-pdf-page "recordstutorial" "$S/https/wiki.portal.chalmers.se/agda/RecordsTutorial.pdf")
(code-pdf-text "recordstutorial" "$S/https/wiki.portal.chalmers.se/agda/RecordsTutorial.pdf")
;; (find-recordstutorialpage)
;; (find-recordstutorialtext)
;; (find-recordstutorialpage 12 "telescope")
;; (find-recordstutorialtext 12 "telescope")
;; (find-recordstutorialpage 13 "Opening a record")
;; (find-recordstutorialtext 13 "Opening a record")
;; (find-recordstutorialpage 14 "Record opening example")
;; (find-recordstutorialtext 14 "Record opening example")
;; (find-recordstutorialpage 18 "Private definitions:")
;; (find-recordstutorialtext 18 "Private definitions:")
;; «wadler-leibniz» (to ".wadler-leibniz")
;; https://homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf
;; https://homepages.inf.ed.ac.uk/wadler/topics/agda.html
(code-pdf-page "wadlerleibniz" "$S/https/homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf")
(code-pdf-text "wadlerleibniz" "$S/https/homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf")
;; (find-wadlerleibnizpage)
;; (find-wadlerleibniztext)
;; (find-wadlerleibnizpage 5 "functional extensionality")
;; (find-wadlerleibniztext 5 "functional extensionality")
;;
;; postulate ext : ∀ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'} {f g : (a : A) → B a}
;; → (∀ (a : A) → f a ≡ g a) → f ≡ g
;; «wadler-smbf» (to ".wadler-smbf")
;; (find-LATEX "catsem-u.bib" "bib-WadlerSMBF")
;; https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
;; https://homepages.inf.ed.ac.uk/wadler/papers/plfa/sbmf.pdf
(code-pdf-page "wadlersmbf" "$S/https/homepages.inf.ed.ac.uk/wadler/papers/plfa/sbmf.pdf")
(code-pdf-text "wadlersmbf" "$S/https/homepages.inf.ed.ac.uk/wadler/papers/plfa/sbmf.pdf")
;; (find-wadlersmbfpage)
;; (find-wadlersmbftext)
;; (find-wadlersmbfpage 11 "writing code with holes")
;; (find-wadlersmbftext 11 "writing code with holes")
(defalias 'qsk 'quail-show-key)
;; (code-c-d "agdastdlib" "~/usrc/agda-stdlib-1.7/")
;; (code-c-d "agdastdlibsrc" "~/usrc/agda-stdlib-1.7/src/")
(code-c-d "agdastdlibsrc" "~/usrc/plfa/standard-library/src/")
;; (find-agdastdlibfile "")
;; (find-agdastdlibsrcfile "")
;; (find-agdastdlibsrcsh "find * | sort")
;; Generated by "agda-mode setup" (but added here by hand).
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
;; «agdamodeel» (to ".agdamodeel")
;; (find-es "agda" "agda2-mode")
;; (find-agdamodeelfile "")
;;
(code-c-d "agdamodeel"
(file-name-directory
(let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")
)
)
)
(code-c-d "agdastack" "~/usrc/agda/.stack-work/install/x86_64-linux-tinfo6/2a9e6669f2e6afa8e70be28c7f28f8856753630b33d317230e7a1e79b8ff317b/8.8.3/share/x86_64-linux-ghc-8.8.3/Agda-2.6.1.3/")
;; (find-agdastackfile "")
;; (find-angg ".emacs" "size")
;; (size 123 56)
;; «glyphs» (to ".glyphs")
;; (find-eevfile "eev-compose-hash.el" "'(ee-composes-do-remove-face)")
;; «C-c-C-SPC» (to ".C-c-C-SPC")
;; (find-es "agda" "C-c-C-SPC")
(keymap-unset rcirc-track-minor-mode-map "C-c C-SPC" 'remove)
;; «hott» (to ".hott")
;; (find-books "__logic/__logic.el" "hott")
(code-pdf-page "hott" "$S/http/saunders.phil.cmu.edu/book/hott-online.pdf")
(code-pdf-text "hott" "$S/http/saunders.phil.cmu.edu/book/hott-online.pdf" 12)
;; «eec-agdalatex» (to ".eec-agdalatex")
;; Tests: (eec-agdalatex-sh0 "Cats3" "RECORD")
;; (eec-agdalatex-sh0 "Cats3" "RECORD")
(defun eec-agdalatex-sh00 (stem &optional record)
(setq record (or record ""))
(ee-template0 "\
echo 'cd ~/LATEX/ &&'
echo 'agda --latex --latex-dir=. {stem}.lagda.tex &&'
echo 'ls -lAF {stem}* &&'
echo 'lualatex {record} {stem}.tex'
echo
cd ~/LATEX/ &&
agda --latex --latex-dir=. {stem}.lagda.tex &&
ls -lAF {stem}* &&
lualatex {record} {stem}.tex"))
(defun eec-agdalatex-sh0 (stem &optional record &rest pos-spec-list)
(apply' find-estring (eec-agdalatex-sh00 stem record) pos-spec-list))
(defun eec-agdalatex-sh (stem &optional record &rest pos-spec-list)
(apply 'find-sh (eec-agdalatex-sh00 stem record) pos-spec-list))
(defun eec-agdalatex-SH (stem &optional record &rest pos-spec-list)
(find-sh (eec-agdalatex-sh00 stem record))
(setq ee-compilation-buffer (buffer-name))
(apply 'ee-goto-position pos-spec-list))
;; (eec-agdalatex-sh0 "FOO")
;;
;; Local Variables:
;; mode: emacs-lisp
;; coding: utf-8-unix
;; End: