Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
####### # # E-scripts on the Lean theorem prover / proof assistant. # # Note 1: use the eev command (defined in eev.el) and the # ee alias (in my .zshrc) to execute parts of this file. # Executing this file as a whole makes no sense. # An introduction to eev can be found here: # # (find-eev-quick-intro) # http://angg.twu.net/eev-intros/find-eev-quick-intro.html # # Note 2: be VERY careful and make sure you understand what # you're doing. # # Note 3: If you use a shell other than zsh things like |& # and the for loops may not work. # # Note 4: I always run as root. # # Note 5: some parts are too old and don't work anymore. Some # never worked. # # Note 6: the definitions for the find-xxxfile commands are on my # .emacs. # # Note 7: if you see a strange command check my .zshrc -- it may # be defined there as a function or an alias. # # Note 8: the sections without dates are always older than the # sections with dates. # # This file is at <http://angg.twu.net/e/lean.e> # or at <http://angg.twu.net/e/lean.e.html>. # See also <http://angg.twu.net/emacs.html>, # <http://angg.twu.net/.emacs[.html]>, # <http://angg.twu.net/.zshrc[.html]>, # <http://angg.twu.net/escripts.html>, # and <http://angg.twu.net/>. # ####### # «.lean4-mode-melpa» (to "lean4-mode-melpa") # «.lean4-mode-vc» (to "lean4-mode-vc") # «.feb2024» (to "feb2024") # «.zulip» (to "zulip") # «.elan» (to "elan") # «.install-2024» (to "install-2024") # «.lean4» (to "lean4") # «.lean4-git» (to "lean4-git") # «.lake» (to "lake") # «.lake-new-greeting» (to "lake-new-greeting") # «.cache-mathlib» (to "cache-mathlib") # «.axiom» (to "axiom") # «.constant» (to "constant") # «.lean4-mode» (to "lean4-mode") # «.lean-mode» (to "lean-mode") # «.mode-line» (to "mode-line") # «.topos» (to "topos") # «.diagram-chasing» (to "diagram-chasing") # «.theorem_proving_in_lean» (to "theorem_proving_in_lean") # «.tpinlean» (to "tpinlean") # «.tpinlean4» (to "tpinlean4") # «.prelude» (to "prelude") # «.rec_on» (to "rec_on") # «.nng4» (to "nng4") # «.natural-number-game» (to "natural-number-game") # «.real-number-game» (to "real-number-game") # «.mathsinlean» (to "mathsinlean") # «.mathzoo» (to "mathzoo") # «.mathlib» (to "mathlib") # «.mathlib4» (to "mathlib4") # «.mathlib4-greeting» (to "mathlib4-greeting") # «.mathlib-calculus» (to "mathlib-calculus") # «.alectryon» (to "alectryon") # «.tactics-in-ND» (to "tactics-in-ND") # «.vernacular» (to "vernacular") # «.fplean4» (to "fplean4") # «.check-fun» (to "check-fun") # # «.anonymous» (to "anonymous") # «.backtick» (to "backtick") # «.double-backtick» (to "double-backtick") # «.calc» (to "calc") # «.def» (to "def") # «.check» (to "check") # «.do-notation» (to "do-notation") # «.elab» (to "elab") # «.explicit-arguments» (to "explicit-arguments") # «.implicit-arguments» (to "implicit-arguments") # «.extern» (to "extern") # «.opaque» (to "opaque") # «.eval» (to "eval") # «.example» (to "example") # «.fun» (to "fun") # «.guillemets» (to "guillemets") # «.import» (to "import") # «.indentation» (to "indentation") # «.inductive» (to "inductive") # «.infix» (to "infix") # «.instance» (to "instance") # «.IO.println» (to "IO.println") # «.IO.Process.output» (to "IO.Process.output") # «.leading_parser» (to "leading_parser") # «.let» (to "let") # «.letterlike» (to "letterlike") # «.match» (to "match") # «.Monad» (to "Monad") # «.namespace» (to "namespace") # «.section» (to "section") # «.open» (to "open") # «.notation» (to "notation") # «.partial» (to "partial") # «.pratt-parser» (to "pratt-parser") # «.print» (to "print") # «.Repr» (to "Repr") # «.ToString» (to "ToString") # «.rw» (to "rw") # «.show» (to "show") # «.string-interpolation» (to "string-interpolation") # «.structure» (to "structure") # «.structures» (to "structures") # «.theorem» (to "theorem") # «.underscore» (to "underscore") # «.variable» (to "variable") # «.delaborator-diagram» (to "delaborator-diagram") # «.reference-manual» (to "reference-manual") # «.metaprogramming» (to "metaprogramming") # «.ullrichmp» (to "ullrichmp") https://leanprover.github.io/ https://leanprover.github.io/tutorial/ https://leanprover.github.io/download/debian78.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # Dependencies sudo apt-get install libstdc++-4.8-dev libgmp-dev libmpfr-dev liblua5.2-dev ninja-build sudo dpkg -i /tmp/lean*.deb # (find-status "lean") # (find-vldifile "lean.list") # (find-udfile "lean/") # (find-sitelispfile "lean/") # (find-sitelispfile "lean/lean-mode.el") # (find-sitelispfile "lean/lean-mode.el" ";; Automatically use lean-mode for") # (find-sitelispfile "lean/load-lean.el") # (find-fline "/usr/lib/lean/") # (find-fline "/usr/lib/lean/hott/") # (find-fline "/usr/lib/lean/hott/book.md") # (find-fline "/usr/lib/lean/library/") # (find-fline "/usr/lib/lean/library/logic/logic.md") https://leanprover.github.io/documentation/ http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf https://leanprover.github.io/tutorial/tutorial.pdf https://leanprover.github.io/tutorial/quickref.pdf https://github.com/leanprover/lean https://github.com/leanprover/lean/blob/master/doc/lean/tutorial.org https://github.com/leanprover/lean/blob/master/src/emacs/README.md https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ *** https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/ https://xenaproject.wordpress.com/2020/06/27/teaching-dependent-type-theory-to-4-year-olds-via-mathematics/amp/ https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/ pictures as eefective guides *** https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/ ##### # # lean4-mode-melpa # 2024mar10 # ##### # «lean4-mode-melpa» (to ".lean4-mode-melpa") # (find-epackage-links 'lean4-mode "lean4mode" t) # (find-epackages 'lean4-mode) # (find-epackage 'lean4-mode) # (package-refresh-contents) # (package-install 'lean4-mode) # (find-epackage 'lean4-mode) # (package-delete (ee-package-desc 'lean4-mode)) # (code-c-d "lean4mode" "~/.emacs.d/elpa/lean4-mode/") # (find-lean4modefile "") ##### # # lean4-mode-vc # 2024mar10 # ##### # «lean4-mode-vc» (to ".lean4-mode-vc") # (find-epackage-links 'lean4-mode "lean4mode" t) # (find-epackage 'lean4-mode) # (package-vc-install "https://github.com/leanprover-community/lean4-mode") # (code-c-d "lean4mode" "~/.emacs.d/elpa/lean4-mode/") # (find-lean4modefile "") ##### # # feb2024 # 2024feb22 # ##### # «feb2024» (to ".feb2024") # (find-es "emacs" "flycheck") # (find-angg "LEAN/a.lean") # (find-fline "~/.emacs.d/elpa/lean4-mode/") # (find-fline "~/.emacs.d/elpa/lean4-mode/lean4-fringe.el" "(require 'lsp-mode)") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) cd ~/.emacs.d/elpa/lean4-mode/ git pull * (byte-recompile-directory "~/.emacs.d/elpa/lean4-mode/") # Source file ‘/home/edrx/.emacs.d/elpa/lean4-mode/lean4-mode.el’ newer than byte-compiled file; using older file # File mode specification error: (file-missing Cannot open load file No such file or directory ht) # (find-efunctiondescr 'byte-compile-file) # (find-efunction 'byte-compile-file) # (find-elnode "Index" "* byte-compile-file:") # (find-efunction-links 'byte-recompile-directory) # (find-epackage-links 'spinner) # (find-epackage-links 'ht) # (find-epackage 'ht) # (code-c-d "ht" "{d}") https://github.com/Wilfred/ht.el ##### # # zulip # 2023jun24 # ##### # «zulip» (to ".zulip") # https://leanprover.zulipchat.com/ ##### # # elan # 2023jun22 # ##### # «elan» (to ".elan") # «install-2024» (to ".install-2024") # (find-angg ".emacs" "lean4") # https://github.com/leanprover/elan # https://proofassistants.stackexchange.com/questions/2/how-do-i-install-lean-4 # (find-git-links "https://github.com/leanprover/elan" "elan") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "/tmp/elan-install/") rm -Rv /tmp/elan-install/ mkdir /tmp/elan-install/ cd /tmp/elan-install/ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \ | sh -s -- --default-toolchain leanprover/lean4:stable # (find-fline "~/.profile") # (find-fline "~/.zprofile") Elan is installed now. Great! To get started you need Elan's bin directory ($HOME/.elan/bin) in your PATH environment variable. Next time you log in this will be done automatically. To configure your current shell run source $HOME/.elan/env # (code-c-d "elan4lean" "~/.elan/toolchains/leanprover--lean4---stable/src/lean/") # (find-elan4leanfile "") # (find-sh "find ~/.elan/ | sort") rm -Rfv ~/.elan/ elan elan show # elan default leanprover/lean4:stable w lake lake # (find-fline "/home/edrx/.elan/bin/") # Welcome to Lean! # # This will download and install Elan, a tool for managing different Lean # versions used in packages you create or download. It will also install a # default version of Lean and its package manager, leanpkg, for editing files not # belonging to any package. # # It will add the leanpkg, lean, and elan commands to Elan's bin directory, # located at: # # /home/edrx/.elan/bin # # This path will then be added to your PATH environment variable by modifying the # profile files located at: # # /home/edrx/.profile # /home/edrx/.zprofile # # You can uninstall at any time with elan self uninstall and these changes will # be reverted. # # Current installation options: # # default toolchain: leanprover/lean4:nightly # modify PATH variable: yes # # 1) Proceed with installation (default) # 2) Customize installation # 3) Cancel installation * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/usrc/elan/ cd ~/usrc/ git clone https://github.com/leanprover/elan cd ~/usrc/elan/ # (code-c-d "elan" "~/usrc/elan/") # (find-elanfile "") # (find-elanfile "elan-init.sh") # (find-fline "~/.elan/") # (find-fline "~/.profile") # (find-fline "~/.zprofile") ##### # # lean4 # 2023jun22 # ##### # «lean4» (to ".lean4") # «lean4-git» (to ".lean4-git") # https://github.com/leanprover/lean4 # https://www.reddit.com/r/haskell/comments/z55hha/review_of_lean_4/ * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/bigsrc/lean4/ cd ~/bigsrc/ git clone https://github.com/leanprover/lean4 cd ~/bigsrc/lean4/ * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) cd ~/bigsrc/lean4/ git pull git clean -dfx git reset --hard find * | sort > .files wc .files export PAGER=cat git branch --list -a git for-each-ref git log --oneline --graph --all -20 # (find-fline "~/bigsrc/") # (find-fline "~/bigsrc/lean4/") # (find-gitk "~/bigsrc/lean4/") # (code-c-d "lean4" "~/bigsrc/lean4/") # (find-lean4sh "find * -type d | sort") # (find-lean4sh "find * | sort | grep -i check") # (find-lean4sh "find * | sort | grep -i notation") # (find-lean4file "") # (find-lean4file ".files") # (find-lean4file "doc/") # (find-lean4file "doc/setup.md") # (find-lean4file "doc/quickstart.md") # (find-lean4file "doc/quickstart.md" "lake init foo") # (find-lean4file "doc/sections.md") # (find-lean4file "doc/dev/mdbook.md") # https://lean-lang.org/lean4/doc/dev/mdbook.html Quickstart: https://github.com/leanprover/lean4/blob/master/doc/quickstart.md Walkthrough installation video: https://www.youtube.com/watch?v=yZo6k48L0VY Quick tour video: https://youtu.be/zyXtbb_eYbY Homepage: https://leanprover.github.io Theorem Proving Tutorial: https://leanprover.github.io/theorem_proving_in_lean4/ Functional Programming in Lean: https://leanprover.github.io/functional_programming_in_lean/ Manual: https://leanprover.github.io/lean4/doc/ Release notes: RELEASES.md Examples: https://leanprover.github.io/lean4/doc/examples.html FAQ: https://leanprover.github.io/lean4/doc/faq.html Setting Up Lean: https://leanprover.github.io/lean4/doc/setup.html https://github.com/leanprover/lean4/blob/master/doc/setup.md#basic-setup $ elan self update # in case you haven't updated elan in a while # download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases) $ elan default leanprover/lean4:stable elan self update elan default leanprover/lean4:stable # download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases) ##### # # lake # 2024mar10 # ##### # «lake» (to ".lake") # (find-angg ".emacs.papers" "fplean4") # (find-angg ".emacs.papers" "fplean4" "75" "Starting a Project") # Deprecated, merged into Lean4: # https://github.com/leanprover/lake # (find-git-links "https://github.com/leanprover/lake" "lake") # (code-c-d "lake" "~/usrc/lake/") # See: (to "IO.Process.output") # (find-lakefile "") # (find-lakefile "README.md") # (find-lakesh "find * | sort") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "/tmp/testlake/") rm -Rv /tmp/testlake/ mkdir /tmp/testlake/ cd /tmp/testlake/ lake new foo find /tmp/testlake/ | sort cd /tmp/testlake/foo/ lake build |& tee olb ** (find-sh "find /tmp/testlake/ | sort") ** (find-sh "find /tmp/testlake/foo/.lake/ | sort") * (code-c-d "foo" "/tmp/testlake/foo/") * (code-c-d "foobuild" "/tmp/testlake/foo/.lake/build/") ** (find-foofile "") ** (find-foobuildfile "") ** (find-foosh "find * | sort") ** (find-foobuildsh "find * | sort") /tmp/testlake/foo/.lake/build/bin/foo cp -v /tmp/testlake/foo/.lake/build/bin/foo /tmp/testlake/foo.bin /tmp/testlake/foo.bin # (find-foofile "") # (find-foofile "Main.lean") # (find-foofile "Foo.lean") # (find-foofile "Foo/") # (find-foofile "Foo/Basic.lean") ##### # # lake-new-greeting # 2023jun25 # ##### # «lake-new-greeting» (to ".lake-new-greeting") # (to "mathlib4-greeting") # (find-angg ".emacs.papers" "fplean4") # (find-fplean4page 75 "Starting a Project") # (find-fplean4text 75 "Starting a Project") # (find-fplean4page 76 "import «Greeting»") # (find-fplean4text 76 "import «Greeting»") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "/tmp/gr/") rm -Rfv /tmp/greeting/ rm -Rfv /tmp/gr/ mkdir /tmp/gr/ cd /tmp/gr/ lake new greeting cd /tmp/gr/greeting/ # lean --run Main.lean # lean --run Greeting.lean find * | sort | tee of0 lake build find * | sort | tee of1 comm of0 of1 laf find build | sort build/bin/greeting cp -v build/bin/greeting /tmp/greeting cd /tmp/ ./greeting # (find-fline "/tmp/gr/greeting/") # (find-fline "/tmp/gr/greeting/Main.lean") # (find-fline "/tmp/gr/greeting/build/bin/") w lake ##### # # cache-mathlib # 2023jun26 # ##### # «cache-mathlib» (to ".cache-mathlib") # (find-fline "~/.cache/mathlib/") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) du -c ~/.cache/mathlib/ find ~/.cache/mathlib/ laf ~/.cache/mathlib/ ##### # # axiom # 2023jun24 # ##### # «axiom» (to ".axiom") # (find-lean-links "axiom") # (find-tpinlean4file "propositions_and_proofs.md" "An \"axiom\" would be a") # (find-tpinlean4file "propositions_and_proofs.md" "constant of such a type.") # (find-lean4pregrep "grep --color=auto -nRH --null -e 'axiom' *") # (find-lean4file "doc/declarations.md" "axiom c : α") # (find-lean4doc "declarations") # (find-lean4docr "declarations") # (find-lean4doc "") # (find-es "agda" "postulates") ##### # # constant # 2023jun24 # ##### # «constant» (to ".constant") # (find-lean4pregrep "grep --color=auto -nRH --null -e constant *") # (find-lean4grep "grep --color=auto -nRH --null -e constant doc/*") # (find-lean4file "doc/funabst.md" "constant f : Nat → Nat") # (find-lean4file "doc/typeobjs.md" "constant α : Type") # (find-lean4file "doc/") # (find-tpinleanpage 11 "constant m : nat") # (find-tpinleantext 11 "constant m : nat") # (find-tpinleanpage (+ 6 5) "2.1 Simple Type Theory") # (find-tpinleantext (+ 6 5) "2.1 Simple Type Theory") # (find-lean4file "doc/simptypes.md" "Simple Type Theory") # (find-lean4file "doc/simptypes.md" "The ``constant`` command") # (find-lean4file "doc/SUMMARY.md" "# Language Manual") # (find-lean4file "doc/SUMMARY.md" "[Theorem Proving in Lean](./tpil.md)") # (find-lean4file "doc/tpil.md") ##### # # lean4-mode # 2023jun22 # ##### # «lean4-mode» (to ".lean4-mode") # https://github.com/leanprover/lean4-mode # (find-es "emacs" "package-vc-install") # (find-es "emacs" "lsp-mode") # (package-vc-install "https://github.com/leanprover/lean4-mode") # (find-epackage-links 'lean4-mode "lean4mode" t) # (find-epackages 'lean4-mode) # (find-epackage 'lean4-mode) # (code-c-d "lean4mode" "~/.emacs.d/elpa/lean4-mode/") # (find-lean4modefile "") # (find-lean4modefile "README.md" "hovering") # (find-lean4modefile "README.md" "C-c C-i" "toggle info view") # (find-lean4modefile "lean4-input.el" "(defcustom lean4-input-inherit") ##### # # lean-mode # 2021jul05 # ##### # «lean-mode» (to ".lean-mode") # (find-epackages 'lean-mode) # (find-epackage-links 'lean-mode) # (find-epackage 'lean-mode) # (code-c-d "leanmode" "~/.emacs.d/elpa/lean-mode-20210502.2049/") # (find-leanmodefile "") # (find-leanmodegrep "grep --color=auto -nH --null -e rootdir *.el") # (find-efunction 'lean-get-rootdir) https://leanprover.github.io/documentation/ https://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf https://leanprover.github.io/tutorial/tutorial.pdf https://leanprover.github.io/tutorial/quickref.pdf ##### # # mode-line # 2024mar10 # ##### # «mode-line» (to ".mode-line") # find-emodeline-links ("%e" mode-line-front-space (:propertize ("" mode-line-mule-info mode-line-client mode-line-modified mode-line-remote mode-line-window-dedicated) display (min-width (6.0))) mode-line-frame-identification mode-line-buffer-identification " " mode-line-position (project-mode-line project-mode-line-format) (vc-mode vc-mode) " " mode-line-modes mode-line-misc-info mode-line-end-spaces) # (find-evardescr 'mode-line-misc-info) # (find-evariable 'mode-line-misc-info) ((which-function-mode (which-func-mode (which-func--use-mode-line ("" which-func-format " ")))) (global-mode-string ("" global-mode-string))) ##### # # topos # 2021jul05 # ##### # «topos» (to ".topos") # https://github.com/b-mehta/topos # (find-git-links "https://github.com/b-mehta/topos" "topos") # (code-c-d "topos" "~/usrc/topos/") # (find-toposfile "") # (find-toposfile "README.md") # (find-toposfile "src/") # (find-toposfile "src/applications/") # (find-toposfile "src/category/") ##### # # diagram-chasing # 2021jul05 # ##### # «diagram-chasing» (to ".diagram-chasing") # (find-books "__cats/__cats.el" "himmel") # (find-himmeldiagchpage 19 "3.2. A formal proof of the four lemma") # (find-himmeldiagchtext 19 "3.2. A formal proof of the four lemma") ##### # # Theorem Proving in Lean4 # 2024mar15 # ##### # «theorem_proving_in_lean» (to ".theorem_proving_in_lean") # «tpinlean» (to ".tpinlean") # «tpinlean4» (to ".tpinlean4") # (find-angg ".emacs.papers" "tpinlean") # https://github.com/leanprover/theorem_proving_in_lean4 # https://leanprover.github.io/theorem_proving_in_lean4/ # https://leanprover.github.io/theorem_proving_in_lean4/print.html # https://leanprover.github.io/theorem_proving_in_lean4/tpinlean4.pdf # (find-git-links "https://github.com/leanprover/theorem_proving_in_lean4" "tpinlean4") # (find-tpinlean4file "SUMMARY.md") ;; <tpinlean4> ;; https://leanprover.github.io/theorem_proving_in_lean4/tpinlean4.pdf ;; (find-fline "$S/https/leanprover.github.io/theorem_proving_in_lean4/") (code-pdf-page "tpinlean4" "$S/https/leanprover.github.io/theorem_proving_in_lean4/tpinlean4.pdf") (code-pdf-text "tpinlean4" "$S/https/leanprover.github.io/theorem_proving_in_lean4/tpinlean4.pdf") ;; (find-tpinlean4page) ;; (find-tpinlean4text) # (code-c-d "tpinlean4" "~/usrc/theorem_proving_in_lean4/") # (find-tpinlean4file "") # (find-tpinlean4file "SUMMARY.md") # (find-tpinlean4file "introduction.md") # (find-tpinlean4file "dependent_type_theory.md") # (find-tpinlean4file "propositions_and_proofs.md") # (find-tpinlean4file "quantifiers_and_equality.md") # (find-tpinlean4file "tactics.md") # (find-tpinlean4file "tactics.md" "C-c C-g") # (find-tpinlean4file "interacting_with_lean.md") # (find-tpinlean4file "inductive_types.md") # (find-tpinlean4file "induction_and_recursion.md") # (find-tpinlean4file "structures_and_records.md") # (find-tpinlean4file "type_classes.md") # (find-tpinlean4file "conv.md") # (find-tpinlean4file "axioms_and_computation.md") # (find-lean4prefile "Init/Data/Nat/Basic.lean") # (find-tpinlean4file "propositions_and_proofs.md" "suffices to show") # (find-tpinlean4page 33 "suffices to show") # (find-tpinlean4text 33 "suffices to show") ##### # # prelude # 2023jun29 # ##### # «prelude» (to ".prelude") # (find-tpinlean4file "inductive_types.md" "prelude") # (find-tpinlean4file "propositions_and_proofs.md" "Prelude.core") # (find-lean4prefile "") # (find-lean4prefile "") # (find-lean4prefile "Init/") # (find-lean4prefile "Init/Prelude.lean") # (find-lean4prefile "Lean/") ##### # # rec_on # 2023jul10 # ##### # «rec_on» (to ".rec_on") # (find-tpinleanpage 89 "nat.rec_on") # (find-tpinleantext 89 "nat.rec_on") # (find-tpinleanpage 102 "weekday.rec_on (also generated automatically)") # (find-tpinleantext 102 "weekday.rec_on (also generated automatically)") # (find-tpinleanpage 103 "renaming option") # (find-tpinleantext 103 "renaming option") https://github.com/leanprover/theorem_proving_in_lean4/blob/master/inductive_types.md inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday #check weekday.sunday #check weekday.monday #check weekday.rec #check weekday.casesOn weekday.casesOn.{u} {motive : weekday → Sort u} (t : weekday) (sunday : motive weekday.sunday) (monday : motive weekday.monday) (tuesday : motive weekday.tuesday) (wednesday : motive weekday.wednesday) (thursday : motive weekday.thursday) (friday : motive weekday.friday) (saturday : motive weekday.saturday) : motive t weekday.rec.{u} {motive : weekday → Sort u} (sunday : motive weekday.sunday) (monday : motive weekday.monday) (tuesday : motive weekday.tuesday) (wednesday : motive weekday.wednesday) (thursday : motive weekday.thursday) (friday : motive weekday.friday) (saturday : motive weekday.saturday) (t : weekday) : motive t @[reducible] inductive mynat : Type | zero : mynat | succ : mynat → mynat -- #check zero #check mynat.zero open mynat (renaming rec_on → rec_on) def add (m n : mynat) : mynat := mynat.rec_on n m (λ n add_m_n => succ add_m_n) #check add #check mynat #check mynat.rec #check mynat.rec_on #check succ zero #check add (succ zero) (succ (succ zero)) -- try it out #reduce add (succ zero) (succ (succ zero)) ##### # # nng4 # 2023jun27 # ##### # «nng4» (to ".nng4") # https://adam.math.hhu.de/ # https://github.com/leanprover-community/lean4game # https://github.com/PatrickMassot/NNG4 ##### # # natural-number-game # 2021oct06 # ##### # «natural-number-game» (to ".natural-number-game") # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html#sourcecode # https://github.com/ImperialCollegeLondon/natural_number_game # https://github.com/mpedramfar/Lean-game-maker # (find-git-links "https://github.com/ImperialCollegeLondon/natural_number_game" "nng") # (find-git-links "https://github.com/mpedramfar/Lean-game-maker" "lgm") # (code-c-d "nng" "~/usrc/natural_number_game/") # (code-c-d "lgm" "~/usrc/Lean-game-maker/") # (find-nngfile "") # (find-nngfile "docs/technical.md") # (find-nngfile "docs/technical.md" "tactic monad") # (find-nngfile "src/tactic/") # (find-nngfile "src/tactic/modded.lean") # (find-nngfile "src/game/") # (find-nngfile "src/game/world2/") # (find-nngfile "src/game/world2/level1.lean") # (find-lgmfile "") https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.youtube.com/watch?v=9V1Xo1n_3Qw LftCM2020: Natural number game - Kevin Buzzard https://xenaproject.wordpress.com/2019/10/24/chalkdust-and-the-natural-number-game/ https://xenaproject.wordpress.com/2019/11/12/the-natural-number-game-an-update/ ##### # # real-number-game # 2021oct17 # ##### # «real-number-game» (to ".real-number-game") # https://github.com/ImperialCollegeLondon/real-number-game # (find-git-links "https://github.com/ImperialCollegeLondon/real-number-game" "rng") # (code-c-d "rng" "~/usrc/real-number-game/") # (find-rngfile "") ##### # # mathsinlean # 2023jun24 # ##### # «mathsinlean» (to ".mathsinlean") # (find-angg ".emacs" "ee-rstdoc-:leanmaths") # (find-angg ".emacs.papers" "mathsinlean") # https://leanprover-community.github.io/mathematics_in_lean/ # https://github.com/leanprover-community/mathematics_in_lean (new) # https://github.com/leanprover-community/mathematics_in_lean3 (old) # (find-git-links "https://github.com/leanprover-community/mathematics_in_lean" "mathsinlean") # (code-c-d "mathsinlean" "~/bigsrc/mathematics_in_lean/") # (find-mathsinleanfile "") # (find-mathsinleanfile "lake-packages/") # (find-mathsinleanfile "MIL/") # (find-mathsinleanfile "MIL/C01_Introduction/") # (find-mathsinleanfile "MIL/C01_Introduction/S02_Overview.lean") # (find-mathsinleanpage) # (find-mathsinleantext) # (find-mathsinleanpage 5 "lake exe cache get") # (find-mathsinleantext 5 "lake exe cache get") # (find-mathsinleangrep "grep --color=auto -nRH --null -e constant *") # (find-lean4mlifile "Mathlib/Util/AssertExists.lean" "elab \"assert_not_exists \"") # file:///home/edrx/bigsrc/mathematics_in_lean/html/C01_Introduction.html * (eepitch-shell3) * (eepitch-kill) * (eepitch-shell3) # (find-sh "du -ch ~/bigsrc/mathematics_in_lean/") du -ch ~/bigsrc/mathematics_in_lean/ rm -Rfv ~/bigsrc/mathematics_in_lean/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathematics_in_lean cd ~/bigsrc/mathematics_in_lean/ lake exe cache get |& tee ole # (find-sh "lake help") # (find-sh "lake help exe") # (find-mathsinleanfile "") # (find-mathsinleanfile "ole") Another basic question... now I have a full copy of mathlib4 in ~/bigsrc/mathlib4/, and I tried to run this: rm -Rfv ~/bigsrc/mathematics_in_lean/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathematics_in_lean cd ~/bigsrc/mathematics_in_lean/ lake exe cache get Apparently 1) this downloaded another full copy of mathlib4 in ~/bigsrc/mathematics_in_lean/lake-packages/mathlib/, and 2) if I create a project and I put a like like this require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" in its lakefile.lean it will also download another full copy of mathlib4... is there a way to make these copies be shared? # Error: LSP :: Yasnippet is not installed, but `lsp-enable-snippet' is set to `t'. You must either install yasnippet, or disable snippet support. LSP :: Connected to [lean4-lsp:187121/starting /home/edrx/bigsrc/mathematics_in_lean]. [2 times] LSP :: Unable to autoconfigure company-mode. [2 times] LSP :: lean4-lsp:187121 initialized successfully in folders: (/home/edrx/bigsrc/mathematics_in_lean) LSP :: You can configure this warning with the `lsp-enable-file-watchers' and `lsp-file-watch-threshold' variables LSP :: Unable to autoconfigure company-mode. [2 times] info: [256/540] Building Aesop.Tree.UnsafeQueue info: [315/794] Building Aesop.Search.Queue info: [353/794] Building Mathlib.Data.ListM.Basic info: [538/794] Building Mathlib.Algebra.Order.Group.Defs error: external command `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean` exited with code 139 `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lake print-paths Init Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Parity Mathlib.Tactic` failed: stderr: info: [155/374] Building Qq.MetaM info: [218/540] Building Std.Data.String.Lemmas info: [256/540] Building Aesop.Tree.UnsafeQueue info: [315/794] Building Aesop.Search.Queue info: [353/794] Building Mathlib.Data.ListM.Basic info: [538/794] Building Mathlib.Algebra.Order.Group.Defs error: > LEAN_PATH=./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./lake-packages/mathlib/build/lib /home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./lake-packages/mathlib/././Mathlib/Algebra/Order/Group/Defs.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Order/Group/Defs.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Order/Group/Defs.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Algebra/Order/Group/Defs.c error: external command `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean` exited with code 139 Mark set ##### # # mathzoo # 2023jun24 # ##### # «mathzoo» (to ".mathzoo") # https://github.com/leanprover-community/mathzoo # (code-c-d "mathzoo" "~/usrc/mathzoo/") # (find-mathzoofile "") # (find-mathzoosh "find * | sort") ##### # # mathlib # 2023jun24 # ##### # «mathlib» (to ".mathlib") # https://github.com/leanprover-community/mathlib # (find-git-links "https://github.com/leanprover-community/mathlib" "mathlib") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv ~/bigsrc/mathlib/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathlib cd ~/bigsrc/mathlib/ # (code-c-d "mathlib" "~/bigsrc/mathlib/") # (find-mathlibfile "") # (find-mathlibfile "README.md") # https://leanprover-community.github.io/install/linux.html ##### # # mathlib4 # 2023jun24 # ##### # «mathlib4» (to ".mathlib4") # https://github.com/leanprover-community/mathlib4 # (find-git-links "https://github.com/leanprover-community/mathlib4" "mathlib4") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv ~/bigsrc/mathlib4/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathlib4 cd ~/bigsrc/mathlib4/ cd ~/bigsrc/mathlib4/ lake exe cache get cd ~/bigsrc/mathlib4/ git clean -dfx git pull elan self update lake build |& tee olb # (code-c-d "mathlib4" "~/bigsrc/mathlib4/") # (find-mathlib4file "") # (find-mathlib4sh "find * | sort") # (find-mathlib4file "README.md") # (find-mathlib4file "README.md" "lean_exe") # (find-mathlib4file "README.md" "elan self update") # (find-mathlib4file "README.md" "lake build") # (find-mathlib4file "" "lake") # (find-mathlib4file "lake-manifest.json") # (find-mathlib4file "lakefile.lean") # (find-mathlib4file "olb") # (find-mathlib4file "lakefile.lean" "package mathlib where") # (find-mathlib4file "Mathlib/Data/Set/") # (find-mathlib4file "Mathlib/Data/Set/Basic.lean") ##### # # mathlib4-greeting # 2023jun26 # ##### # «mathlib4-greeting» (to ".mathlib4-greeting") # (to "lake-new-greeting") # (find-mathlib4file "README.md" "require mathlib from git") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv /tmp/gr/ mkdir /tmp/gr/ cd /tmp/gr/ lake new greeting cd /tmp/gr/greeting/ lake build lake update lake build # (find-fline "/tmp/gr/greeting/") ##### # # mathlib-calculus # 2022jul03 # ##### # «mathlib-calculus» (to ".mathlib-calculus") # https://github.com/leanprover-community/mathlib # https://leanprover-community.github.io/mathlib_docs/ # https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html # https://leanprover-community.github.io/get_started.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/usrc/mathlib/ cd ~/usrc/ git clone https://github.com/leanprover-community/mathlib git clone git@github.com:leanprover-community/mathematics_in_lean.git cd ~/usrc/mathlib/ cd ~/usrc/mathlib/ In a terminal, navigate to the folder where you want to put a copy of the repository, and type git clone git@github.com:leanprover-community/mathematics_in_lean.git to fetch it from github. Navigate to mathematics_in_lean, and execute lake exe cache get to fetch a compiled version of the library, mathlib. Type code . to open the folder in VS Code. Alternatively, you can run VS Code and choose Open Folder from the File menu. Be sure to open the folder mathematics_in_lean, not any other folder. ;; <leanmathlib> ;; "The Lean Mathematical Library" ;; https://arxiv.org/abs/1910.09336 ;; https://arxiv.org/pdf/1910.09336.pdf (code-pdf-page "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") (code-pdf-text "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") ;; (find-leanmathlibpage) ;; (find-leanmathlibtext) # (find-anggsh "find . -mtime 0 | sort") # (find-fline "~/.config/Code/") # (find-fline "~/.local/pipx/logs/") # (find-fline "~/.elan/") # (find-fline "~/.local/pipx/") # (find-fline "~/.mathlib/") # (find-fline "~/.mathlib/url") # (find-fline "~/.vscode/") ##### # # alectryon # 2024mar24 # ##### # «alectryon» (to ".alectryon") # https://github.com/cpitclaudel/alectryon # https://proofassistants.stackexchange.com/questions/62/is-there-software-for-interfacing-lean-code-with-latex # https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Literate.20programming.20in.20Lean4.20.2F.20Lean4.20.2B.20Org.20mode.html ##### # # tactics-in-ND # 2021oct14 # ##### # «tactics-in-ND» (to ".tactics-in-ND") # https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Deduction/near/257611457 # https://leanprover-community.github.io/mathlib_docs/tactic/explode.html#tactic.explode ##### # # vernacular # 2021dec16 # ##### # «vernacular» (to ".vernacular") # https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista # https://www.youtube.com/watch?v=Dp-mQ3HxgDE#t=1h0m0s ##### # # fplean4 # 2023jun02 # ##### # «fplean4» (to ".fplean4") # (find-angg ".emacs.papers" "fplean4") # https://news.ycombinator.com/item?id=36107796 Functional Programming in Lean – a book on using Lean 4 to write programs (leanprover.github.io) # https://leanprover.github.io/functional_programming_in_lean/ # https://leanprover.github.io/functional_programming_in_lean/print.html # (code-pdf-page "fplean4" "$S/https/leanprover.github.io/Functional Programming in Lean.pdf") # (code-pdf-text "fplean4" "$S/https/leanprover.github.io/Functional Programming in Lean.pdf") # (find-fplean4page) # (find-fplean4text) ##### # # check-fun # 2023jun24 # ##### # «check-fun» (to ".check-fun") # (to "check") # (find-lean4pregrep "grep --color=auto -nRH --null -e '#check' *") -- (find-fplean4page 12 "#eval (1 + 2 : Nat)") -- (find-fplean4text 12 "#eval (1 + 2 : Nat)") -- (find-fplean4page 13 "#check (1 - 2 : Int)") -- (find-fplean4text 13 "#check (1 - 2 : Int)") -- (find-fplean4page 15 "#check add1") -- (find-fplean4text 15 "#check add1") -- (find-fplean4page 15 "#check (add1)") -- (find-fplean4text 15 "#check (add1)") -- (find-fplean4page 54 "#check fun (x : Int) => x + 1") -- (find-fplean4text 54 "#check fun (x : Int) => x + 1") -- (find-fplean4page 55 "(· + 1)") -- (find-fplean4text 55 "(· + 1)") -- (find-lean4file "doc/functions.md") #check 1 #check 1 : Int -- bad #check (1 : Int) -- good #check Nat #check Nat -> Nat #check ((Nat -> Nat) : Type) #check ( Nat -> Nat : Type) #check fun x => x + 1 #check fun (x : Nat) => x + 1 #check ((fun (x : Nat) => x + 1) : (Nat -> Nat)) #check (· + 1) #check ((· + 1) : (Nat -> Nat)) ##### # # anonymous # 2024mar23 # ##### # «anonymous» (to ".anonymous") # (find-tpinlean4page 29 "anonymous constructor") # (find-tpinlean4text 29 "anonymous constructor") # (find-tpinlean4page 33 "anonymous constructor") # (find-tpinlean4text 33 "anonymous constructor") # (find-fplean4page 202 "anonymous angle-bracket notation") # (find-fplean4text 202 "anonymous angle-bracket notation") ##### # # backtick # 2024mar29 # ##### # «backtick» (to ".backtick") # «double-backtick» (to ".double-backtick") # (find-leanmetadoc "main/05_syntax#matching-on-syntax") # (find-leanmetadocr "main/05_syntax#matching-on-syntax") # (find-leanmetadocr "main/05_syntax#matching-on-syntax" "`(Nat.add $x $y)") # (find-leanmetadoc "main/03_expressions#constructing-expressions") # (find-lean-links "backtick") # (find-angg "LEAN/syntax.lean" "mini-project") ##### # # calc # 2024apr06 # ##### # «calc» (to ".calc") # (find-tpinlean4page 45 "Calculational Proofs") # (find-tpinlean4text 45 "Calculational Proofs") # (find-tpinlean4page 45 "with the keyword calc") # (find-tpinlean4text 45 "with the keyword calc") # (find-tpinlean4file "quantifiers_and_equality.md") # (find-tpinlean4file "quantifiers_and_equality.md" "Calculational Proofs") # (find-lean-links "calc") # (find-lean-links "Calc") # (find-lean4presh "find * | sort") # (find-lean4presh "find * | sort | grep Calc") ##### # # def # 2024mar09 # ##### # «def» (to ".def") # (find-fplean4page 15 "def maximum (n : Nat) (k : Nat) : Nat :=") # (find-fplean4text 15 "def maximum (n : Nat) (k : Nat) : Nat :=") # (find-tpinlean4-links "Definitions") (find-tpinlean4file "dependent_type_theory.md" "## Definitions") def add0 : Nat := 4 def add1 (n : Nat) : Nat := n + 1 def add2 (n : Nat) (m : Nat) : Nat := n + m def add3 (n : Nat) (m : Nat) : Nat := n + m #eval add0 #eval add1 7 #eval add2 3 4 #eval add3 3 4 ##### # # #check # 2024mar28 # ##### # «check» (to ".check") # (to "check-fun") # (find-lean-links "check") # (find-lean-links ">>") # (find-fplean4page 13 "use #check instead of #eval") # (find-fplean4text 13 "use #check instead of #eval") # (find-lean4prefile "Lean/Parser/Command.lean" "@[builtin_command_parser] def check") ##### # # do notation # 2024mar23 # ##### # «do-notation» (to ".do-notation") # (to "Monad") # (find-lean4doc "do") # (find-lean4doc "do#the-do-notation") # (find-lean4docr "do" "# The `do` notation") # (find-lean4docrfile "do.md") # (find-fplean4page 66 "Combining IO Actions") # (find-fplean4text 66 "Combining IO Actions") # (find-fplean4page 67 "let bindings in do use a left arrow") # (find-fplean4text 67 "let bindings in do use a left arrow") # (find-fplean4page 90 "do Notation") # (find-fplean4text 90 "do Notation") # (find-lean4prefile "Lean/Elab/Do.lean") # (find-lean4prefile "Lean/Parser/Do.lean") ##### # # elab # 2024mar30 # ##### # «elab» (to ".elab") # (find-leanmetadoc "main/01_intro#building-a-command") # (find-leanmetadocrfile "main/01_intro.lean" "elab \"#assertType \"") # (find-leanmetadocrfile "main/01_intro.lean" "inductive Arith : Type where") ##### # # explicit-arguments # 2024mar15 # ##### # «explicit-arguments» (to ".explicit-arguments") # «implicit-arguments» (to ".implicit-arguments") # (find-tpinlean4file "dependent_type_theory.md" "Implicit Arguments") # (find-tpinlean4file "dependent_type_theory.md" "``@foo``" "made explicit") # (find-fplean4page 38 "Implicit Arguments") # (find-fplean4text 38 "Implicit Arguments") # (find-fplean4page 39 "#check List.length (α := Int)") # (find-fplean4text 39 "#check List.length (α := Int)") ##### # # extern # 2024mar23 # ##### # «extern» (to ".extern") # «opaque» (to ".opaque") # (find-lean4prefile "Init/System/IO.lean" "@[extern \"lean_get_stdin\"] opaque getStdin") # (find-lean4grep "grep --color=auto -nRH --null -e lean_get_stdin *") # (find-lean4file "stage0/src/runtime/io.cpp" "lean_get_stdin") ##### # # #eval # 2024mar09 # ##### # «eval» (to ".eval") # (find-fplean4page 12 "#eval (1 + 2 : Nat)") # (find-fplean4text 12 "#eval (1 + 2 : Nat)") # (find-fplean4page 88 "Running IO Actions With #eval") # (find-fplean4text 88 "Running IO Actions With #eval") ##### # # example # 2024mar11 # ##### # «example» (to ".example") # (to "metaprogramming") # (find-angg ".emacs.papers" "tpinlean4" "The example command") # (find-tpinlean4page 29 "The example command") # (find-tpinlean4text 29 "The example command") # (find-lean4pregrep "grep --color=auto -nRH --null -e example *") # (find-lean4pregrep "grep --color=auto -nRH --null -e Parser.Command *") # (find-lean4pregrep "grep --color=auto -nRH --null -e Lean.Parser *") # (find-lean4pregrep "grep --color=auto -nRH --null -e Lean.Parser.Command *") # (find-lean4prefile "Lean/Elab/DefView.lean" "def | theorem | example | opaque | abbrev") # (find-lean4prefile "Lean/Elab/DeclarationRange.lean" "Parser.Command.«example»") ##### # # fun # 2024mar22 # ##### # «fun» (to ".fun") # (find-tpinlean4file "dependent_type_theory.md" "`fun` (or `λ`)") # (find-tpinlean4file "propositions_and_proofs.md" "``(fun x => t) s`` and ``t[s/x]``") # (find-fplean4page 54 "Anonymous Functions") # (find-fplean4text 54 "Anonymous Functions") # (find-fplean4page 55 "centered dot") # (find-fplean4text 55 "centered dot") ##### # # guillemets # 2024mar23 # ##### # «guillemets» (to ".guillemets") # (find-fplean4page 76 "guillemets around a name") # (find-fplean4text 76 "guillemets around a name") ##### # # import # 2024mar31 # ##### # «import» (to ".import") # (find-lean-links "import") # (find-fplean4page 76 "The import line") # (find-fplean4text 76 "The import line") # (find-fplean4page 77 "Libraries and Imports") # (find-fplean4text 77 "Libraries and Imports") # (find-lean4pregrep "grep --color=auto -nRH --null -e import *") ##### # # indentation # 2024mar09 # ##### # «indentation» (to ".indentation") # (find-fplean4page 87 "semicolon" "curly braces") # (find-fplean4text 87 "semicolon" "curly braces") # (find-fplean4page 88 "This version uses only whitespace-sensitive layout") # (find-fplean4text 88 "This version uses only whitespace-sensitive layout") ##### # # inductive # 2024mar23 # ##### # «inductive» (to ".inductive") # (find-fplean4page 26 "inductive Bool where") # (find-fplean4text 26 "inductive Bool where") # (find-fplean4page 129 "inductive BinTree") # (find-fplean4text 129 "inductive BinTree") ##### # # infix # 2024mar11 # ##### # «infix» (to ".infix") # (find-fplean4page 153 "Infix Operators") # (find-fplean4text 153 "Infix Operators") # (find-fplean4page 153 "infixl:55 \" ~~> \" => andThen") # (find-fplean4text 153 "infixl:55 \" ~~> \" => andThen") ##### # # instance # 2024mar14 # ##### # «instance» (to ".instance") # (to "Repr") # (find-fplean4page 104 "instance : Plus Nat where") # (find-fplean4text 104 "instance : Plus Nat where") # (find-tpinlean4page 157 "Type Classes") # (find-tpinlean4text 157 "Type Classes") # (find-tpinlean4page 160 "Chaining Instances") # (find-tpinlean4text 160 "Chaining Instances") # (find-lean4doc "typeclass") # (find-lean4docr "typeclass") # (find-lean4docrfile "typeclass.md" "## Chaining Instances") ##### # # IO.println # 2024mar22 # ##### # «IO.println» (to ".IO.println") # (find-fplean4page 106 "IO.println") # (find-fplean4text 106 "IO.println") ##### # # IO.Process.output # 2024mar11 # ##### # «IO.Process.output» (to ".IO.Process.output") # (find-lean4prefile "Init/System/IO.lean" "Run process to completion") # (find-lean4prefile "lake/Lake/Config/InstallPath.lean") # (find-lean4prefile "lake/Lake/Config/InstallPath.lean" "let out ← IO.Process.output {") # (find-lean4pregrep "grep --color=auto -nirH --null -e pipe *") # (find-lean4pregrep "grep --color=auto -nirH --null -e Process.Stdio.piped *") # https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/IO.2EProcess.2Eoutput.20with.20stdin.20being.20a.20string.3F # (find-lean4prefile "") IO.Process.output with stdin being a string? Hi all! How do I tell IO.Process.output to run with its stdin being (piped from) a string? Or, more precisely: how do I write a function "tac" that receives a string, pipes it through /usr/bin/tac, and returns the output? Apparently the "def findLeanSysroot?" in Lake/Config/InstallPath.lean is a good starting point, and I would need to use IO.Process.Stdio.piped somewhere - but I am a newbie and I'm struggling with the details... Note: I mentioned tac above just to discuss a minimal example, but my real objective is to use this thing here - luatree.lua - to draw 2D trees in ASCII art... here's a screenshot: https://github.com/leanprover/lean4/blob/master/src/lake/Lake/Config/InstallPath.lean#L121 http://anggtwu.net/eev-maxima.html#luatree ##### # # leading_parser # 2024mar27 # ##### # «leading_parser» (to ".leading_parser") # (find-lean-links "leading_parser") # (find-lean4pregrep "grep --color=auto -nRH --null -e 'leading_parser' *") # (find-lean4prefile "Lean/Elab/BuiltinNotation.lean" "invalid `leading_parser` macros") # (find-lean4prefile "Lean/Parser/Syntax.lean" "def «precedence» := leading_parser") ##### # # let # 2024mar09 # ##### # «let» (to ".let") # (find-fplean4page 50 "let") # (find-fplean4text 50 "let") # (find-fplean4page 50 "let rec") # (find-fplean4text 50 "let rec") # (find-fplean4page 67 "definition using :=") # (find-fplean4text 67 "definition using :=") # (find-fplean4page 67 "let bindings in do use a left arrow") # (find-fplean4text 67 "let bindings in do use a left arrow") ##### # # letterlike # 2024apr06 # ##### # «letterlike» (to ".letterlike") # (find-lean-links "unicode") # (find-lean-links "letterlike") # (find-lean4docrfile "lexical_structure.md") # (find-lean4docrfile "lexical_structure.md" "letterlike_symbols") # (find-lean4pregrep "grep --color=auto -niRH --null -e 'unicode' *") # (find-lean4pregrep "grep --color=auto -niRH --null -e 'letterlike' *") ##### # # match # 2024mar10 # ##### # «match» (to ".match") # (find-angg ".emacs.papers" "fplean4" "28" "Pattern Matching") # (find-angg ".emacs.papers" "fplean4" "57" "if let") # (find-fplean4page 28 "Pattern Matching") # (find-fplean4text 28 "Pattern Matching") # (find-fplean4page 57 "if let") # (find-fplean4text 57 "if let") #eval match 2 with | 0 => true | (n + 1) => false #eval match 2 with | 0 => true | (_ + 1) => false #eval match 2 with | 0 => true | (_ + 1) => false ##### # # Monad # 2024mar24 # ##### # «Monad» (to ".Monad") # (to "do-notation") # (find-lean4prefile "Init/Prelude.lean" "class Bind") # (find-lean4prefile "Init/Prelude.lean" "class Pure") # (find-lean4prefile "Init/Prelude.lean" "class Functor") # (find-lean4prefile "Init/Prelude.lean" "class Applicative") # (find-lean4prefile "Init/Prelude.lean" "class Monad") # https://lean-lang.org/lean4/doc/monads/intro.html # https://lean-lang.org/lean4/doc/monads/functors.lean.html # https://lean-lang.org/lean4/doc/monads/applicatives.lean.html # https://lean-lang.org/lean4/doc/monads/monads.lean.html # https://lean-lang.org/lean4/doc/monads/laws.lean.html # (find-lean4file "doc/monads/laws.lean") # (find-fplean4page 71 "def twice (action : IO Unit) : IO Unit") # (find-fplean4text 71 "def twice (action : IO Unit) : IO Unit") # (find-fplean4page 79 "Worked Example: cat") # (find-fplean4text 79 "Worked Example: cat") # (find-fplean4page 164 "The Monad Type Class") # (find-fplean4text 164 "The Monad Type Class") # (find-fplean4page 165 "General Monad Operations") # (find-fplean4text 165 "General Monad Operations") ##### # # namespace # 2024mar15 # ##### # «namespace» (to ".namespace") # «section» (to ".section") # «open» (to ".open") # (find-lean-links "namespace") # (find-angg ".emacs.papers" "tpinlean4" "15" "2.7. Namespaces") # (find-angg ".emacs.papers" "tpinlean4" "83" "6.3. More on Namespaces") # (find-tpinlean4page 15 "2.7. Namespaces") # (find-tpinlean4text 15 "Namespaces") # (find-tpinlean4page 16 "The open command") # (find-tpinlean4text 16 "The open command") # (find-tpinlean4page 83 "6.3. More on Namespaces") # (find-tpinlean4text 83 "More on Namespaces") # (find-tpinlean4file "dependent_type_theory.md" "# Namespaces") # (find-tpinlean4file "interacting_with_lean.md" "More on Namespaces") # (find-lean4doc "sections") # (find-lean4doc "namespaces") # (find-lean4doc "tour#functions-and-namespaces") # (find-lean4docrfile "namespaces.md" "# Namespaces") # (find-lean4docrfile "tour.md" "# Functions and Namespaces") # (find-angg ".emacs.papers" "fplean4" "56" "Namespaces") # (find-fplean4page 56 "Namespaces") # (find-fplean4text 56 "Namespaces") # (find-tpinlean4file "type_classes.md" "open scoped <namespace>") ##### # # notation # 2024mar28 # ##### # «notation» (to ".notation") # (find-lean-links "notation") # (find-tpinlean4grep "grep --color=auto -nH --null -e 'notation' *.md") # (find-tpinlean4file "interacting_with_lean.md" "notation ``≤`` to the `isPrefix` relation") # (find-tpinlean4file "interacting_with_lean.md" "notation:65 lhs:65 \" + \" rhs:66") # (find-tpinlean4file "tactics.md" "The notation ``←t``") # (find-tpinlean4file "type_classes.md" "how the notation `a*b` is defined in Lean") # (find-lean4docgrep "grep --color=auto -nRH --null -e 'notation' *") # (find-leanmetadocrgrep "grep --color=auto -nRH --null -e 'notation' *") # (find-lean4prefile "Init/Notation.lean" "\" ∧ \"") # (find-leanmetadoc "main/03_expressions#constructing-expressions" "double backticks") # (find-leanmetadoc "main/05_syntax") # (find-leanmetadoc "main/05_syntax#free-form-syntax-declarations" "scoped syntax") ##### # # partial # 2024mar23 # ##### # «partial» (to ".partial") # (find-fplean4page 80 "The dump function is declared partial") # (find-fplean4text 80 "The dump function is declared partial") ##### # # Pratt parser # 2024mar27 # ##### # «pratt-parser» (to ".pratt-parser") # (to "ullrichmp") # (find-lean4pregrep "grep --color=auto -nRH --null -e 'pratt' *") # (find-lean4prefile "Lean/Parser/Basic.lean" "def prattParser") ##### # # #print # 2024mar11 # ##### # «print» (to ".print") # (find-fplean4page 190 "#print Nat") # (find-fplean4text 190 "#print Nat") # (find-fplean4page 191 "#print IO.Error") # (find-fplean4text 191 "#print IO.Error") # (find-tpinlean4grep "grep --color=auto -nH --null -e '#print' *.md") # (find-tpinleanpage (+ 6 89) "6.8 Displaying Information") # (find-tpinleantext (+ 6 89) "6.8 Displaying Information") # (find-lean4prefile "Lean/Parser/Command.lean" "@[builtin_command_parser] def print") # (find-lean-links "#print") #print definition : display definition #print inductive : display an inductive type and its constructors #print notation : display all notation #print notation <tokens> : display notation using any of the tokens #print axioms : display assumed axioms #print options : display options set by user #print prefix <namespace> : display all declarations in the namespace #print classes : display all classes #print instances <class name> : display all instances of the given class #print fields <structure> : display all fields of a structure ##### # # Repr and ToString # 2024mar24 # ##### # «Repr» (to ".Repr") # «ToString» (to ".ToString") # (to "instance") # (find-fplean4page 106 "ToString") # (find-fplean4text 106 "ToString") # (find-lean4presh "find * | sort") # (find-lean4presh "find * | sort | grep Repr") # (find-lean4prefile "Init/Data/Repr.lean") # (find-lean4prefile "Lean/Elab/Deriving/Repr.lean") # (find-lean4presh "find * | sort | grep -i tostring") # (find-lean4prefile "Init/Data/ToString.lean") # (find-lean4prefile "Init/Data/ToString/Basic.lean") # (find-lean4prefile "Init/Data/ToString/Macro.lean") ##### # # rw # 2024mar14 # ##### # «rw» (to ".rw") # (find-lean4rc1file "Init/Tactics.lean" "macro (name := rwSeq) \"rw\"") # (find-mathsinleanpage 9 "2.1 Calculating") # (find-mathsinleantext 9 "2.1 Calculating") # (find-mathsinleanpage 9 "2.1 Calculating" "tactic rw") # (find-mathsinleantext 9 "2.1 Calculating" "tactic rw") # (find-leanmathsdoc "C02_Basics#calculating") # (find-mathsinleanfile "MIL/C02_Basics/S01_Calculating.lean") ##### # # show # 2024mar22 # ##### # «show» (to ".show") # (find-lean-links "show") # (find-tpinlean4file "propositions_and_proofs.md" "show p from hp") # (find-lean4prefile "Init/Prelude.lean" "`show T' from e` is sugar for") # (find-lean4prefile "Init/Tactics.lean" "`show t` finds the first goal") ##### # # s!"str" # 2024mar23 # ##### # «string-interpolation» (to ".string-interpolation") # (find-fplean4page 59 "String Interpolation") # (find-fplean4text 59 "String Interpolation") # (find-fplean4page 106 "when a value occurs in an interpolated string") # (find-fplean4text 106 "when a value occurs in an interpolated string") # (find-lean4prefile "Lean/Parser/StrInterpolation.lean") ##### # # structures # 2023jun24 # ##### # «structure» (to ".structure") # «structures» (to ".structures") # (find-fplean4page 18 "Structures") # (find-fplean4text 18 "Structures") # (find-fplean4page 20 "structure Point3D where") # (find-fplean4text 20 "structure Point3D where") # (find-fplean4page 24 "The function Point.modifyBoth") # (find-fplean4text 24 "The function Point.modifyBoth") # (find-tpinlean4page 106 "structure Prod") # (find-tpinlean4text 106 "structure Prod") # (find-tpinlean4page 152 "Declaring Structures") # (find-tpinlean4text 152 "Declaring Structures") # (find-tpinlean4file "inductive_types.md" "structure Prod") # (find-anggfile "LEAN/structures1.lean") structure Point where x : Float y : Float deriving Repr structure Point3D where x : Float y : Float z : Float deriving Repr def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 } --#check { x := 0.0, y := 0.0 } -- err #check ({ x := 0.0, y := 0.0 } : Point) #check { x := 0.0, y := 0.0 : Point} ##### # # theorem # 2024mar27 # ##### # «theorem» (to ".theorem") # (find-tpinlean4page 25 "the theorem command") # (find-tpinlean4text 25 "the theorem command") # (find-lean4prefile "Init/Tactics.lean" "This simp theorem") # (find-lean4prefile "Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean" "marked with the `congr` attribute") # (find-lean4prefile "Lean/Elab/DefView.lean" "leading_parser \"theorem \"") # (find-lean4prefile "Lean/Elab/Declaration.lean" "Lean.Parser.Command.theorem") # (find-lean4prefile "Lean/Elab/Tactic/Simp.lean" "using the simp theorems collected in `ctx`") # (find-lean4prefile "Lean/Parser/Command.lean" "def «theorem»") ##### # # underscore # 2024apr06 # ##### # «underscore» (to ".underscore") # (find-tpinlean4page 36 "you can use an underscore _") # (find-tpinlean4text 36 "you can use an underscore _") # (find-tpinlean4page 21 "holes") # (find-tpinlean4text 21 "holes") # (find-tpinlean4page 87 "replaced by @t _") # (find-tpinlean4text 87 "replaced by @t _") variable (P Q R : Prop) theorem triv1 (p : P) : P := p theorem triv2 («.P» : P) : P := «.P» theorem triv3 («.P» : P) («P→Q» : P → Q) : Q := _ theorem triv4 («.P» : P) («P→Q» : P → Q) : Q := «P→Q» _ theorem triv5 («.P» : P) («P→Q» : P → Q) : Q := «P→Q» «.P» ##### # # variable # 2024mar15 # ##### # «variable» (to ".variable") # (find-lean-links "the ``variable`` command") # (find-tpinlean4file "dependent_type_theory.md" "The ``variable`` command") # (find-tpinlean4file "dependent_type_theory.md" "Variables can also be specified as implicit") # (find-tpinlean4file "propositions_and_proofs.md" "variable (p q r : Prop)") # (find-tpinlean4file "propositions_and_proofs.md" "variable {p : Prop}") # https://lean-lang.org/lean4/doc/sections.html # (find-lean4file "doc/sections.md" "``section``") # (find-lean4file "doc/sections.md") # (find-lean4prefile "Lean/Parser/Command.lean" "@[builtin_command_parser] def «variable»") ##### # # delaborator-diagram # 2024mar10 # ##### # «delaborator-diagram» (to ".delaborator-diagram") # https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Pretty-printing.20of.20sums/near/355279588 # https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Pretty-printing.20of.20sums/near/355262783 # # String ---(parser)---> Syntax ---(elaborator)---> Expr ---(delaborator)---> Syntax ---(formatter)---> String # # parser elaborator delaborator formatter # String --------> Syntax ------------> Expr -------------> Syntax -----------> String ##### # # reference-manual # 2024mar09 # ##### # «reference-manual» (to ".reference-manual") # https://leanprover.github.io/reference/ # (find-leanrefdocw "using_lean#using-lean-with-emacs") # (find-leanrefdocw "declarations") # https://github.com/leanprover/reference # https://leanprover.github.io/reference/lean_reference.pdf (code-pdf-page "leanref" "$S/https/leanprover.github.io/reference/lean_reference.pdf") (code-pdf-text "leanref" "$S/https/leanprover.github.io/reference/lean_reference.pdf") ;; (find-leanrefpage) ;; (find-leanreftext) ##### # # metaprogramming # 2024mar09 # ##### # «metaprogramming» (to ".metaprogramming") # (find-angg ".emacs" "ee-rstdoc-:leanmeta") # https://leanprover-community.github.io/lean4-metaprogramming-book/md/ # https://github.com/leanprover-community/ # https://github.com/leanprover-community/lean4-metaprogramming-book # (find-git-links "https://github.com/leanprover-community/lean4-metaprogramming-book" "leanmeta") # (code-c-d "leanmeta" "~/usrc/lean4-metaprogramming-book/") # (find-leanmetafile "") # (find-leanmetash "find * | sort") # (find-leanmetash "cd lean; find * | sort") # (find-leanmetafile "lean/main/01_intro.lean") # (find-wgetrecursive-links "https://leanprover-community.github.io/lean4-metaprogramming-book/") # (find-leanmetadoc "") # (find-leanmetadoc "main/01_intro#book-structure") # (find-leanmetadoc "main/05_syntax") # (find-leanmetadoc "main/05_syntax") # (find-leanmetadoc "main/04_metam#full-normalisation") # (find-leanmetadoc "main/04_metam#constructing-expressions") # (find-leanmetadocr "main/04_metam#constructing-expressions") # (find-leanmetadocw "main/04_metam#constructing-expressions") # (find-leanmetadoc "main/04_metam#deconstructing-expressions") # (find-leanmetadoc "main/06_macros") # (find-leanmetadoc "main/03_expressions") # (find-leanmetadocrfile "main/07_elaboration.lean") ##### # # Sebastian Ullrich: Lean Together 2021 - Metaprogramming in Lean 4 # 2024mar11 # ##### # «ullrichmp» (to ".ullrichmp") # (to "pratt-parser") https://www.researchgate.net/scientific-contributions/Sebastian-Ullrich-2132232638 https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/lt2021/ https://leanprover-community.github.io/lt2021/schedule.html *** https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf https://leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf https://leanprover-community.github.io/lt2021/slides/sebastian-An-Overview-of-Lean-4-Demo.pdf # (code-video "ullrichmpvideo" "/sda5/videos/Lean_Together_2021_-_Metaprogramming_in_Lean_4-hxQ1vvhYN_U.webm") # (find-ullrichmpvideo "0:00") # (find-ullrichmpvideo "6:50" "notation") # (find-ullrichmpvideo "8:45" "trace.Elab.command") # (find-ullrichmpvideo "9:30" "for the next command") # (find-ullrichmpvideo "12:00" "longest parse wins") # (find-ullrichmpvideo "26:45" "crosses") (code-pdf-page "ullrichmp" "$S/https/leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf") (code-pdf-text "ullrichmp" "$S/https/leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf") ;; (find-ullrichmppage) ;; (find-ullrichmptext) # (find-ullrichmppage 13 "precedence (Pratt) parser") # (find-ullrichmptext 13 "precedence (Pratt) parser") # (find-leanmetadoc "md/main/05_syntax#declaration-helpers" "longest parse") stdout.putStrLn # (find-fplean4page 76 "import «Greeting»") # (find-fplean4text 76 "import «Greeting»") https://leanprover-community.github.io/lean4-metaprogramming-book/md/main/01_intro.html#introducing-notation-defining-new-syntax Proposition world. A Proposition is a true/false statement, like 2 + 2 = 4 or 2 + 2 = 5. Just like we can have concrete sets in Lean like mynat, and abstract sets called things like X, we can also have concrete propositions like 2 + 2 = 5 and abstract propositions called things like P. Mathematicians are very good at conflating a theorem with its proof. They might say "now use theorem 12 and we're done". What they really mean is "now use the proof of theorem 12..." (i.e. the fact that we proved it already). Particularly problematic is the fact that mathematicians use the word Proposition to mean "a relatively straightforward statement which is true" and computer scientists use it to mean "a statement of arbitrary complexity, which might be true or false". Computer scientists are far more careful about distinguishing between a proposition and a proof. For example: x + 0 = x is a proposition, and add_zero x is its proof. The convention we'll use is capital letters for propositions and small letters for proofs. https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html https://github.com/ImperialCollegeLondon/natural_number_game https://github.com/mpedramfar/Lean-game-maker https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ Picking a basis and then pretending you didn’t https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/zulip.md https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Calling.20lean.20from.20command.20line https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf (find-books "__comp/__comp.el" "colton") https://leanprover.github.io/reference/ https://leanprover.github.io/reference/using_lean.html#using-lean-with-emacs https://lawrencecpaulson.github.io/2023/01/18/Sqrt2_irrational.html https://news.ycombinator.com/item?id=34437735 Formalising a new proof that the square root of two is irrational (lawrencecpaulson.github.io) *** https://news.ycombinator.com/item?id=35511152 What I've Learned About Formal Methods in Half a Year (jakob.space) ;; <schemesinlean> ;; https://arxiv.org/abs/2101.02602 ;; https://arxiv.org/pdf/2101.02602.pdf (code-pdf-page "schemesinlean" "$S/https/arxiv.org/pdf/2101.02602.pdf") (code-pdf-text "schemesinlean" "$S/https/arxiv.org/pdf/2101.02602.pdf") ;; (find-schemesinleanpage) ;; (find-schemesinleantext) https://proofassistants.stackexchange.com/questions/2153/type-theory-lean-3-to-lean-4 ;; <ullrichmhm> ;; https://arxiv.org/abs/2001.10490 ;; https://arxiv.org/pdf/2001.10490.pdf ;; Ullrich/Moura: "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages" (code-pdf-page "ullrichmhm" "$S/https/arxiv.org/pdf/2001.10490.pdf") (code-pdf-text "ullrichmhm" "$S/https/arxiv.org/pdf/2001.10490.pdf") ;; (find-ullrichmhmpage) ;; (find-ullrichmhmtext) # (find-ullrichmhmpage 13 "token antiquotation %$x") # (find-ullrichmhmtext 13 "token antiquotation %$x") ;; <leanteach2020> ;; https://github.com/vaibhavkarve/leanteach2020 ;; https://vaibhavkarve.github.io/leanteach_report.pdf ;; https://wiki.illinois.edu/wiki/display/LT2020/LeanTeach+2020+Home ;; Dolcos/Kong/Zhao/Phillips/Karve: "Interactive Theorem Proving in Lean" (code-pdf-page "leanteach2020" "$S/https/vaibhavkarve.github.io/leanteach_report.pdf") (code-pdf-text "leanteach2020" "$S/https/vaibhavkarve.github.io/leanteach_report.pdf") (code-c-d "leanteach2020" "~/usrc/leanteach2020/") (code-video "leanteach2020video" "~/usrc/leanteach2020/igl_talk.mp4") ;; (find-leanteach2020page) ;; (find-leanteach2020text) # (find-git-links "https://github.com/vaibhavkarve/leanteach2020" "leanteach2020") # (find-leanteach2020file "") # (find-leanteach2020video) # (find-leanteach2020video "0:00") ;; <carneiro> https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf https://github.com/digama0/lean-type-theory/releases/download/v1.0/slides.pdf https://github.com/digama0/lean-type-theory/archive/refs/tags/v1.0.tar.gz https://www.youtube.com/watch?v=3sKrSNhSxik https://pp.ipd.kit.edu/person.php?id=144 Dr.-Ing. Sebastian Ullrich https://www.math.uni-bonn.de/ag/logik/events/MLPTT/Ullrich_lean.pdf Embedding Languages into Lean 4 ;; <ullrichemb> ;; https://www.math.uni-bonn.de/ag/logik/events/MLPTT/Ullrich_lean.pdf ;; (find-fline "$S/https/www.math.uni-bonn.de/ag/logik/events/MLPTT/") (code-pdf-page "ullrichemb" "$S/https/www.math.uni-bonn.de/ag/logik/events/MLPTT/Ullrich_lean.pdf") (code-pdf-text "ullrichemb" "$S/https/www.math.uni-bonn.de/ag/logik/events/MLPTT/Ullrich_lean.pdf") ;; (find-ullrichembpage) ;; (find-ullrichembtext) https://leanprover.github.io/presentations/20181012_MSR/#/4 https://leanprover-community.github.io/lt2021/slides/sebastian-An-Overview-of-Lean-4-Demo.pdf https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ elaborator https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/ https://leanprover.github.io/papers/lean4.pdf https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Metaprogramming.20tutorial.html https://github.com/leanprover-community/quote4 https://leanprover-community.github.io/undergrad.html https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/Exponential.html#NormedSpace.exp https://leanprover-community.github.io/mathlib-overview.html https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Yoneda.html#CategoryTheory.yoneda https://leanprover-community.github.io/theories/category_theory.html https://github.com/ImperialCollegeLondon/formalising-mathematics-2024 https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Project.20idea.3A.20linking.20MathLib.20to.20math.20books https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/idiom.20for.20using.20calc.20to.20rewrite.20the.20goal https://github.com/leanprover-community/lean4-samples/blob/main/RubiksCube/README.md https://lean-lang.org/lean4/doc/examples/widgets.lean.html https://github.com/leanprover-community/lean4-samples/blob/main/ListComprehension/README.md https://github.com/leanprover-community/lean4-samples/blob/main/GuessMyNumber/README.md (find-lean4prefile "Init/Prelude.lean" "triangle") # Local Variables: # coding: utf-8-unix # End: