|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
;; This file:
;; http://anggtwu.net/.emacs.lean.el.html
;; http://anggtwu.net/.emacs.lean.el
;; (find-angg ".emacs.lean.el")
;; Author: Eduardo Ochs <eduardoochs@gmail.com>
;;
;; (defun ele () (interactive) (find-angg ".emacs.lean.el"))
;; (find-angg ".emacs" "lean4")
;; (find-angg ".emacs.templates" "find-leanrstdoc-links")
;; (load (buffer-file-name))
;; Main:
;; «.ee-leandoc-:lean4» (to "ee-leandoc-:lean4")
;; «.ee-rstdoc-:lean4» (to "ee-rstdoc-:lean4")
;; «.ee-leandoc-:tpil4» (to "ee-leandoc-:tpil4")
;; «.ee-rstdoc-:tpil4» (to "ee-rstdoc-:tpil4")
;; «.ee-leandoc-:leanmeta» (to "ee-leandoc-:leanmeta")
;; «.ee-rstdoc-:leanmeta» (to "ee-rstdoc-:leanmeta")
;; «.ee-leandoc-:fplean4» (to "ee-leandoc-:fplean4")
;; «.ee-rstdoc-:fplean4» (to "ee-rstdoc-:fplean4")
;; «.ee-leandoc-:leanref» (to "ee-leandoc-:leanref")
;; «.ee-rstdoc-:leanref» (to "ee-rstdoc-:leanref")
;; «.ee-leandoc-:leanmaths» (to "ee-leandoc-:leanmaths")
;; «.ee-rstdoc-:leanmaths» (to "ee-rstdoc-:leanmaths")
;; «.ee-leandoc-:mechprf» (to "ee-leandoc-:mechprf")
;; «.ee-rstdoc-:mechprf» (to "ee-rstdoc-:mechprf")
;; «.lt2021leo» (to "lt2021leo")
;; «.lt2021leom» (to "lt2021leom")
;; «.lt2021sebastianleo» (to "lt2021sebastianleo")
;;; _ __ __ _
;;; | | ___ __ _ _ __ | \/ | __ _ _ __ _ _ __ _| |
;;; | | / _ \/ _` | '_ \ | |\/| |/ _` | '_ \| | | |/ _` | |
;;; | |__| __/ (_| | | | | | | | | (_| | | | | |_| | (_| | |
;;; |_____\___|\__,_|_| |_| |_| |_|\__,_|_| |_|\__,_|\__,_|_|
;;;
;; «ee-leandoc-:lean4» (to ".ee-leandoc-:lean4")
(setq ee-leandoc-:lean4
'(:kw "lean4"
:kill "ldk"
:base-web "https://lean-lang.org/lean4/doc/"
:git-repo "https://github.com/leanprover/lean4"
:usrc "~/bigsrc/"
:base-rst "~/bigsrc/lean4/doc/"
:base "whatIsLean"
:rst ""
))
;; (find-2a nil '(find-leanrstdoc-links ee-leandoc-:lean4))
;; (find-2a nil '(find-leanprint-links ee-leandoc-:lean4))
(code-pdf-page "lean4" "$S/https/lean-lang.org/lean4/doc/print.pdf")
(code-pdf-text8 "lean4" "$S/https/lean-lang.org/lean4/doc/print.pdf")
;; (find-lean4page)
;; (find-lean4text)
;; «ee-rstdoc-:lean4» (to ".ee-rstdoc-:lean4")
;; Skels: (find-rstdoc-links :lean4)
;; See: (find-es "lean" ":lean4")
;; Try: (find-lean4doc "whatIsLean")
;; (find-lean4docw "whatIsLean")
;; (find-lean4docr "whatIsLean.md")
;; (find-lean4docrfile "")
;; (find-lean4doc "metaprogramming-arith")
;; (find-lean4docr "metaprogramming-arith.lean")
;; (find-lean4docr "metaprogramming-arith.md")
;; (find-lean4docrfile "" "metaprogramming-arith")
(setq ee-rstdoc-:lean4
'(:base "whatIsLean"
:base-web "https://lean-lang.org/lean4/doc/"
:base-html "file:///home/edrx/snarf/https/lean-lang.org/lean4/doc/"
:base-rst "~/bigsrc/lean4/doc/"
:rst ""
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^lean-lang.org/lean4/doc/"
"^bigsrc/lean4/doc/")
:kill ldk
))
;; (find-code-rstdoc :lean4)
(code-rstdoc :lean4)
;;; _____ _ ____
;;; |_ _| |__ ___ ___ _ __ ___ _ __ ___ | _ \ _ __ _____ __
;;; | | | '_ \ / _ \/ _ \| '__/ _ \ '_ ` _ \ | |_) | '__/ _ \ \ / /
;;; | | | | | | __/ (_) | | | __/ | | | | | | __/| | | (_) \ V /
;;; |_| |_| |_|\___|\___/|_| \___|_| |_| |_| |_| |_| \___/ \_/
;;;
;; «ee-leandoc-:tpil4» (to ".ee-leandoc-:tpil4")
(setq ee-leandoc-:tpil4
'(:kw "tpil4"
:kill "tpk"
:rst ".md"
:base-web "https://lean-lang.org/theorem_proving_in_lean4/"
:git-repo "https://github.com/leanprover/theorem_proving_in_lean4"
:git-subdir ""
:base "introduction"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:tpil4))
;; (find-2a nil '(find-leanprint-links 'ee-leandoc-:tpil4))
(code-pdf-page "tpil4" "$S/https/lean-lang.org/theorem_proving_in_lean4/print.pdf")
(code-pdf-text8 "tpil4" "$S/https/lean-lang.org/theorem_proving_in_lean4/print.pdf")
;; (find-tpil4page)
;; (find-tpil4text)
;; «ee-rstdoc-:tpil4» (to ".ee-rstdoc-:tpil4")
;; Skels: (find-rstdoc-links :tpil4)
;; See: (find-es "lean" ":tpil4")
;; Try: (find-tpil4doc "introduction")
;; (find-tpil4docw "introduction")
;; (find-tpil4docr "introduction")
;; (find-tpil4docrfile "")
(setq ee-rstdoc-:tpil4
'(:base "introduction"
:base-web "https://lean-lang.org/theorem_proving_in_lean4/"
:base-html "file:///home/edrx/snarf/https/lean-lang.org/theorem_proving_in_lean4/"
:base-rst "~/usrc/theorem_proving_in_lean4/"
:rst ".md"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^lean-lang.org/theorem_proving_in_lean4/"
"^usrc/theorem_proving_in_lean4/")
:kill tpk
))
;; (find-code-rstdoc :tpil4)
(code-rstdoc :tpil4)
;;; __ __ _
;;; | \/ | ___| |_ __ _ _ __ _ __ ___ __ _
;;; | |\/| |/ _ \ __/ _` | '_ \| '__/ _ \ / _` |
;;; | | | | __/ || (_| | |_) | | | (_) | (_| |
;;; |_| |_|\___|\__\__,_| .__/|_| \___/ \__, |
;;; |_| |___/
;;
;; «ee-leandoc-:leanmeta» (to ".ee-leandoc-:leanmeta")
(setq ee-leandoc-:leanmeta
'(:kw "leanmeta"
:kill "lmk"
:rst ".lean"
:base-web "https://leanprover-community.github.io/lean4-metaprogramming-book/"
:git-repo "https://github.com/leanprover-community/lean4-metaprogramming-book"
:git-subdir "lean/"
:base "main/01_intro"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:leanmeta))
;; (find-2a nil '(find-leanprint-links 'ee-leandoc-:leanmeta))
(code-pdf-page "leanmeta" "$S/https/leanprover-community.github.io/lean4-metaprogramming-book/print.pdf")
(code-pdf-text8 "leanmeta" "$S/https/leanprover-community.github.io/lean4-metaprogramming-book/print.pdf")
;; (find-leanmetapage)
;; (find-leanmetatext)
;; «ee-rstdoc-:leanmeta» (to ".ee-rstdoc-:leanmeta")
;; Skels: (find-rstdoc-links :leanmeta)
;; See: (find-es "lean" ":leanmeta")
;; Try: (find-leanmetadoc "main/01_intro")
;; (find-leanmetadocw "main/01_intro")
;; (find-leanmetadocr "main/01_intro")
;; (find-leanmetadocrfile "")
;; (find-leanmetapage)
;; (find-leanmetatext)
(setq ee-rstdoc-:leanmeta
'(:base "main/01_intro"
:base-web "https://leanprover-community.github.io/lean4-metaprogramming-book/"
:base-html "file:///home/edrx/snarf/https/leanprover-community.github.io/lean4-metaprogramming-book/"
:base-rst "~/usrc/lean4-metaprogramming-book/lean/"
:rst ".lean"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^leanprover-community.github.io/lean4-metaprogramming-book/"
"^usrc/lean4-metaprogramming-book/lean/")
:kill lmk
))
;; (find-code-rstdoc :leanmeta)
(code-rstdoc :leanmeta)
;;; _____ _ _ _
;;; | ___| _ _ __ ___| |_(_) ___ _ __ __ _| |
;;; | |_ | | | | '_ \ / __| __| |/ _ \| '_ \ / _` | |
;;; | _|| |_| | | | | (__| |_| | (_) | | | | (_| | |
;;; |_| \__,_|_| |_|\___|\__|_|\___/|_| |_|\__,_|_|
;;;
;; «ee-leandoc-:fplean4» (to ".ee-leandoc-:fplean4")
(setq ee-leandoc-:fplean4
'(:kw "fplean4"
:kill "fpk"
:rst ".md"
:base-web "https://lean-lang.org/functional_programming_in_lean/"
:git-repo "https://github.com/leanprover/fp-lean"
:git-subdir "functional-programming-lean/src/"
:base "introduction"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:fplean4))
;; (find-2a nil '(find-leanprint-links 'ee-leandoc-:fplean4))
(code-pdf-page "fplean4" "$S/https/lean-lang.org/functional_programming_in_lean/print.pdf")
(code-pdf-text8 "fplean4" "$S/https/lean-lang.org/functional_programming_in_lean/print.pdf")
;; (find-fplean4page)
;; (find-fplean4text)
;; «ee-rstdoc-:fplean4» (to ".ee-rstdoc-:fplean4")
;; Skels: (find-rstdoc-links :fplean4)
;; See: (find-es "lean" ":fplean4")
;; Try: (find-fplean4doc "introduction")
;; (find-fplean4docw "introduction")
;; (find-fplean4docr "introduction")
;; (find-fplean4docrfile "")
(setq ee-rstdoc-:fplean4
'(:base "introduction"
:base-web "https://lean-lang.org/functional_programming_in_lean/"
:base-html "file:///home/edrx/snarf/https/lean-lang.org/functional_programming_in_lean/"
:base-rst "~/usrc/fp-lean/functional-programming-lean/src/"
:rst ".md"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^lean-lang.org/functional_programming_in_lean/"
"^usrc/fp-lean/functional-programming-lean/src/")
:kill fpk
))
;; (find-code-rstdoc :fplean4)
(code-rstdoc :fplean4)
(code-c-d "fplean4" "~/usrc/fp-lean/")
(code-c-d "fplean4doc" "$S/https/lean-lang.org/functional_programming_in_lean/")
;; (find-fplean4file "")
;; (find-fplean4docfile "")
;;; ____ __
;;; | _ \ ___ / _| ___ _ __ ___ _ __ ___ ___
;;; | |_) / _ \ |_ / _ \ '__/ _ \ '_ \ / __/ _ \
;;; | _ < __/ _| __/ | | __/ | | | (_| __/
;;; |_| \_\___|_| \___|_| \___|_| |_|\___\___|
;;;
;; «ee-leandoc-:leanref» (to ".ee-leandoc-:leanref")
(setq ee-leandoc-:leanref
'(:kw "leanref"
:kill "lrk"
:base-web "https://leanprover.github.io/reference/"
:base-rst "$S/https/leanprover.github.io/reference/_sources/"
:base "index"
:rst ".rst.txt"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:leanref))
;; «ee-rstdoc-:leanref» (to ".ee-rstdoc-:leanref")
;; Skels: (find-rstdoc-links :leanref)
;; See: (find-es "lean" ":leanref")
;; Try: (find-leanrefdoc "index")
;; (find-leanrefdocw "index")
;; (find-leanrefdocr "index")
;; (find-leanrefdoc "using_lean#using-lean-with-emacs")
;; (find-leanrefdocw "using_lean#using-lean-with-emacs")
;; (find-leanrefdocr "using_lean#using-lean-with-emacs")
;; (find-leanrefdocrfile "")
(setq ee-rstdoc-:leanref
'(:base "index"
:base-web "https://leanprover.github.io/reference/"
:base-html "file:///home/edrx/snarf/https/leanprover.github.io/reference/"
:base-rst "$S/https/leanprover.github.io/reference/_sources/"
:rst ".rst.txt"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^leanprover.github.io/reference/"
"^$S/https/leanprover.github.io/reference/_sources/")
:kill lrk
))
;; (find-code-rstdoc :leanref)
(code-rstdoc :leanref)
;;; __ __ _ _ _ _
;;; | \/ | __ _| |_| |__ ___ (_)_ __ | | ___ __ _ _ __
;;; | |\/| |/ _` | __| '_ \/ __| | | '_ \ | | / _ \/ _` | '_ \
;;; | | | | (_| | |_| | | \__ \ | | | | | | |__| __/ (_| | | | |
;;; |_| |_|\__,_|\__|_| |_|___/ |_|_| |_| |_____\___|\__,_|_| |_|
;;;
;; «ee-leandoc-:leanmaths» (to ".ee-leandoc-:leanmaths")
(setq ee-leandoc-:leanmaths
'(:kw "leanmaths"
:kill "lmak"
:base-web "https://leanprover-community.github.io/mathematics_in_lean/"
:git-repo "https://github.com/avigad/mathematics_in_lean_source"
:base-rst "~/bigsrc/mathematics_in_lean_source/MIL/"
:base "index"
:rst ".lean"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:leanmaths))
;; «ee-rstdoc-:leanmaths» (to ".ee-rstdoc-:leanmaths")
;; Skels: (find-rstdoc-links :leanmaths)
;; See: (find-es "lean" ":leanmaths")
;; Try: (find-leanmathsdoc "index")
;; (find-leanmathsdocw "index")
;; (find-leanmathsdocr "index")
;; (find-leanmathsdocrfile "")
;; (find-leanmathsdoc "C02_Basics#calculating")
;; (find-leanmathsdocw "C02_Basics#calculating")
;; (find-leanmathsdocr "C02_Basics/S01_Calculating")
(setq ee-rstdoc-:leanmaths
'(:base "index"
:base-web "https://leanprover-community.github.io/mathematics_in_lean/"
:base-html "file:///home/edrx/snarf/https/leanprover-community.github.io/mathematics_in_lean/"
:base-rst "~/bigsrc/mathematics_in_lean_source/MIL/"
:rst ".lean"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^leanprover-community.github.io/mathematics_in_lean/"
"^bigsrc/mathematics_in_lean_source/MIL/")
:kill lmak
))
;; (find-code-rstdoc :leanmaths)
(code-rstdoc :leanmaths)
;;; __ __ _ ____ __
;;; | \/ | ___ ___| |__ | _ \ _ __ / _|
;;; | |\/| |/ _ \/ __| '_ \ | |_) | '__| |_
;;; | | | | __/ (__| | | | | __/| | | _|
;;; |_| |_|\___|\___|_| |_| |_| |_| |_|
;;;
;; «ee-leandoc-:mechprf» (to ".ee-leandoc-:mechprf")
(setq ee-leandoc-:mechprf
'(:kw "mechprf"
:kill "mpk"
:base-web "https://hrmacbeth.github.io/math2001/"
;;:base-rst "$S/https/hrmacbeth.github.io/math2001/_sources/"
:git-repo "https://github.com/hrmacbeth/math2001"
:git-subdir "Math2001/"
:base "index"
:rst ".rst.txt"
))
;; (find-2a nil '(find-leanrstdoc-links 'ee-leandoc-:mechprf))
;; «ee-rstdoc-:mechprf» (to ".ee-rstdoc-:mechprf")
;; Skels: (find-rstdoc-links :mechprf)
;; See: (find-es "lean" ":mechprf")
;; Try: (find-mechprfdoc "index")
;; (find-mechprfdocw "index")
;; (find-mechprfdocr "index")
;; (find-mechprfdocrfile "")
(setq ee-rstdoc-:mechprf
'(:base "index"
:base-web "https://hrmacbeth.github.io/math2001/"
:base-html "file:///home/edrx/snarf/https/hrmacbeth.github.io/math2001/"
:base-rst "~/usrc/math2001/Math2001/"
:rst ".rst.txt"
:res ("#.*$" "\\?.*$"
"\\.html$" "\\.txt$" "\\.rst$" "\\.md$" "\\.lean$"
"^file://+" "^/" "^home/edrx/" "^~/" "^snarf/" "^https:?/+"
"^hrmacbeth.github.io/math2001/"
"^usrc//")
:kill mpk
))
;; (find-code-rstdoc :mechprf)
(code-rstdoc :mechprf)
;; «lt2021leo» (to ".lt2021leo")
;; "Lean 4 - an overview"
;; https://leanprover-community.github.io/lt2021/schedule.html
;; https://leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf
(code-pdf-page "lt2021leo" "$S/https/leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf")
(code-pdf-text "lt2021leo" "$S/https/leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf")
;; (find-lt2021leopage)
;; (find-lt2021leotext)
;; «lt2021leom» (to ".lt2021leom")
;; "Lean 4 - metaprogramming"
;; https://leanprover-community.github.io/lt2021/schedule.html
;; https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf
(code-pdf-page "lt2021leom" "$S/https/leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf")
(code-pdf-text "lt2021leom" "$S/https/leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf")
;; (find-lt2021leompage)
;; (find-lt2021leomtext)
;; «lt2021sebastianleo» (to ".lt2021sebastianleo")
;; (find-youtubedl-links "/sda5/videos/" "Lean_Together_2021_-_Metaprogramming_in_Lean_4" "hxQ1vvhYN_U" ".webm" "lt2021sebastianleo")
(code-video "lt2021sebastianleovideo" "/sda5/videos/Lean_Together_2021_-_Metaprogramming_in_Lean_4-hxQ1vvhYN_U.webm")
;; (find-lt2021sebastianleovideo)
;; (find-lt2021sebastianleovideo "0:00")
;; http://www.youtube.com/watch?v=UeGvhfW1v9M Lean Together 2021: An overview of Lean 4
;; Local Variables:
;; coding: utf-8-unix
;; End: