|
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")
# «.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")
# «.mathsinlean-source» (to "mathsinlean-source")
# «.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")
# «.axiom» (to "axiom")
# «.command» (to "command")
# «.constant» (to "constant")
# «.backtick» (to "backtick")
# «.double-backtick» (to "double-backtick")
# «.calc» (to "calc")
# «.def» (to "def")
# «.check» (to "check")
# «.checksyntax» (to "checksyntax")
# «.company» (to "company")
# «.discard» (to "discard")
# «.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")
# «.have» (to "have")
# «.import» (to "import")
# «.indentation» (to "indentation")
# «.inductive» (to "inductive")
# «.inductive-Arith» (to "inductive-Arith")
# «.inductive-Expr» (to "inductive-Expr")
# «.inductive-List» (to "inductive-List")
# «.inductive-Nat» (to "inductive-Nat")
# «.inductive-Option» (to "inductive-Option")
# «.inductive-Syntax» (to "inductive-Syntax")
# «.infix» (to "infix")
# «.instance» (to "instance")
# «.interpolatedStr» (to "interpolatedStr")
# «.IO.println» (to "IO.println")
# «.IO.Process.output» (to "IO.Process.output")
# «.latin-cross» (to "latin-cross")
# «.leading_parser» (to "leading_parser")
# «.lean-type-theory» (to "lean-type-theory")
# «.let» (to "let")
# «.letterlike» (to "letterlike")
# «.match» (to "match")
# «.minted» (to "minted")
# «.Monad» (to "Monad")
# «.namespace» (to "namespace")
# «.section» (to "section")
# «.open» (to "open")
# «.notation» (to "notation")
# «.orelse» (to "orelse")
# «.partial» (to "partial")
# «.pratt-parser» (to "pratt-parser")
# «.print» (to "print")
# «.Repr» (to "Repr")
# «.ToString» (to "ToString")
# «.rw» (to "rw")
# «.scoped-syntax» (to "scoped-syntax")
# «.show» (to "show")
# «.string-interpolation» (to "string-interpolation")
# «.structure» (to "structure")
# «.structures» (to "structures")
# «.tagged-subgoals» (to "tagged-subgoals")
# «.telescopes» (to "telescopes")
# «.termParser» (to "termParser")
# «.theorem» (to "theorem")
# «.toolchains» (to "toolchains")
# «.try-catch» (to "try-catch")
# «.typeof» (to "typeof")
# «.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-lean4sh "find * | sort | grep -i synthesize")
# (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/
#####
#
# 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
#####
#
# mathsinlean-source
# 2024apr28
#
#####
# «mathsinlean-source» (to ".mathsinlean-source")
# https://github.com/avigad/mathematics_in_lean_source
# https://leanprover-community.github.io/mathematics_in_lean/
# (find-git-links "https://github.com/avigad/mathematics_in_lean_source" "mathsinleansrc")
# (code-c-d "mathsinleansrc" "~/usrc/mathematics_in_lean_source/")
# (find-mathsinleansrcfile "")
# (find-mathsinleansrcfile "Makefile")
# https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Recommended.20ways.20to.20convert.20Lean4.20code.20to.20LaTeX.3F/near/435827430
#####
#
# 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")
#####
#
# 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")
# (find-tpinlean4page 26 "the axiom declaration")
# (find-tpinlean4text 26 "the axiom declaration")
#####
#
# command
# 2024may12
#
#####
# «command» (to ".command")
# (find-lean4prefile "Init/Notation.lean" "def command : Category := {}")
# (find-leanmetadoc "main/01_intro#building-a-command")
#####
#
# 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")
#####
#
# 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")
# (find-lean4pregrep "grep --color=auto -nRH --null -e '\"def \"' *")
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")
# (to "scoped-syntax")
# (find-lean-links "check")
# (find-lean-links ">>")
# (find-fplean4page 13 "use #check instead of #eval")
# (find-fplean4text 13 "use #check instead of #eval")
# (find-fplean4page 51 "#check 14")
# (find-fplean4text 51 "#check 14")
# (find-fplean4page 52 "#check (14 : Int)")
# (find-fplean4text 52 "#check (14 : Int)")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'check' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e '#check' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e '<|>' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'namespace Command' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'builtin_command_parser' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'elaboration function for' *")
# (find-lean4prefile "Lean/Parser/Command.lean" "@[builtin_command_parser] def check")
# (find-lean4prefile "Lean/Parser/Command.lean" "\"#check \" >> termParser")
#####
#
# #checksyntax
# 2024may15
#
#####
# «checksyntax» (to ".checksyntax")
# (find-leanmetadoc "main/05_syntax#free-form-syntax-declarations")
# (find-leanmetadocw "main/05_syntax#free-form-syntax-declarations")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'elaboration function for' *")
# (find-lean4prefile "Lean/Elab/Command.lean" "elaboration function for")
# (find-lean4prefile "Lean/Elab/Term.lean" "elaboration function for")
# https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20do.20I.20write.20a.20.22.23check_syntax.22.3F/near/438919441
Hi all,
I'm taking far too long to do this myself, so I decided to ask...
In the section "Free form syntax declarations" of the metaprogramming
book there's an example - inside "namespace Playground2" - in which
the command "#check_failure ⊥ OR (⊤ AND ⊥)" fails with the error
"elaboration function for 'Playground2.term_OR_' has not been
implemented". I only found that error message in two places in the
source:
here in Lean/Elab/Command.lean, and
here in Lean/Elab/Term.lean,
but lots of things happen before that error message...
How do I write a variant of #check or #check_failure - let me call
that variant "#check_syntax" - that parses the rest of the line like
#check or #check_failure, i.e., like this,
@[builtin_command_parser] def check := leading_parser "#check " >> termParser
but that does not try to elaborate the result of "termParser"? I would
like it to just print the resulting Syntax object...
---
Neat! If I run this,
#check `(42 + "foo")
then the output is:
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
{
raw :=
Lean.Syntax.node3 info `term_+_ (Lean.Syntax.node1 info `num (Lean.Syntax.atom info "42"))
(Lean.Syntax.atom info "+")
(Lean.Syntax.node1 info `str (Lean.Syntax.atom info "\"foo\"")) } : ?m.233 (Lean.TSyntax `term) (lsp)
I would still like to learn how to write a new command that works as
the first half of #check, but that helps!
If anyone else is reading this, here is a version that is trivial to run:
import Lean.Elab.Command
namespace Playground2
scoped syntax "⊥" : term
scoped syntax "⊤" : term
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term
elab "#check_syntax " t:term : command => do Lean.logInfo m!"{t}"
elab "#check_syntax " t:term : command => do Lean.logInfo m!"{repr t.raw}"
#check_syntax ⊥ OR (⊤ AND ⊥)
end Playground2
The definition of "#check_syntax" that holds is the last one - to change its behavior, reorder the "elab" lines.
#####
#
# company
# 2024may07
#
#####
# «company» (to ".company")
# (find-es "emacs" "company")
# (find-companyfile "company-capf.el")
#####
#
# discard
# 2024may12
#
#####
# «discard» (to ".discard")
# (find-leanmetadoc "main/01_intro#building-a-command")
# (find-leanmetadocr "main/01_intro" "### Building a command")
# (find-lean4prefile "Init/Control/Basic.lean" "def Functor.discard")
#####
#
# 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)")
# (find-fplean4page 48 "Automatic Implicit Arguments")
# (find-fplean4text 48 "Automatic Implicit Arguments")
#####
#
# 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»")
variable (p q : Prop)
example (hp : p) (hq : q) : p ∧ q := And.intro hp hq
example (_ : Int) := 42
example (_ : Int) : Int := 42
variable (P Q R : Prop)
variable {P Q R : Prop}
variable {p : P}
variable {q : Q}
example (p : P) (q : Q) : P ∧ Q := And.intro p q
#check fun (p : P) (q : Q) => And.intro p q
#####
#
# 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")
# (find-lean4prefile "Lean/Parser/Term.lean" "@[builtin_term_parser] def «fun»")
# (find-lean4prefile "Lean/Elab/Binders.lean" "@[builtin_term_elab «fun»]")
# (find-lean4prefile "Lean/Parser/Basic.lean" "def unicodeSymbol")
#check fun x => x + 1
#check fun (x : Int) => x + 1
#check fun {α : Type} (x : α) => x
#check fun x y => x + y
#check fun (x : Int) y => x + y
#check fun (x : Int) (y : Int) => x + y
#check fun (x y : Int) => x + y
#check (fun x y => x + y : Int → Int → Int)
#check 42
#check (42 : Int)
#####
#
# guillemets
# 2024mar23
#
#####
# «guillemets» (to ".guillemets")
# (find-fplean4page 76 "guillemets around a name")
# (find-fplean4text 76 "guillemets around a name")
#####
#
# have
# 2024apr30
#
#####
# «have» (to ".have")
# (find-lean-links "have")
# (find-angg ".emacs.papers" "tpinlean4")
# (find-tpinlean4file "propositions_and_proofs.md" "the ``have`` construct")
# (find-tpinlean4page 33 "3.4. Introducing Auxiliary Subgoals")
# (find-tpinlean4text 33 "Introducing Auxiliary Subgoals")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'have' *")
# (find-lean4prefile "Lean/Elab/Do.lean" "def getDoHaveVars (doHave : Syntax)")
variable (P Q : Prop)
example (paq : P ∧ Q) : Q ∧ P :=
have p : P := paq.left
have q : Q := paq.right
show Q ∧ P from And.intro q p
#####
#
# 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")
# (find-lean4prefile "Lean/Elab/Declaration.lean" "leading_parser \"inductive \"")
#####
#
# inductive-Arith
# 2024may12
#
#####
# «inductive-Arith» (to ".inductive-Arith")
# (find-leanmetadoc "main/01_intro#building-a-dsl-and-a-syntax-for-it")
# (find-leanmetadocr "main/01_intro" "### Building a DSL and a syntax for it")
# (find-lean4prefile "Lean/Parser/Syntax.lean" "declare_syntax_cat")
# (find-lean4prefile "Lean/Parser/Syntax.lean" "def catBehavior :=")
# (find-lean4prefile "Lean/Elab/Syntax.lean" "@[builtin_command_elab «syntax»]")
# (find-lean4prefile "Lean/Elab/MacroRules.lean" "@[builtin_command_elab «macro_rules»]")
# (find-lean4prefile "Lean/Parser/Syntax.lean" "@[builtin_command_parser] def «syntax»")
# (find-lean4prefile "Lean/Parser/Syntax.lean" "@[builtin_command_parser] def «macro_rules»")
#####
#
# inductive-Expr
# 2024may12
#
#####
# «inductive-Expr» (to ".inductive-Expr")
# (find-leanmetadoc "main/03_expressions")
# (find-leanmetadocr "main/03_expressions")
# https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Creating.20Expr.20objects
#####
#
# inductive-List
# 2024may13
#
#####
# «inductive-List» (to ".inductive-List")
# (find-fplean4page 37 "inductive List")
# (find-fplean4text 37 "inductive List")
# (find-lean4prefile "Init/Prelude.lean" "inductive List")
# (find-lean4prefile "Init/Data/List/Basic.lean" "syntax \"[\"")
# (find-lean4prefile "Init/Notation.lean" "@[inherit_doc] infixr:67 \" :: \" => List.cons")
#####
#
# inductive-Nat
# 2024may13
#
#####
# «inductive-Nat» (to ".inductive-Nat")
# (find-fplean4page 27 "inductive Nat")
# (find-fplean4text 27 "inductive Nat")
# (find-fplean4page 31 "def plus")
# (find-fplean4text 31 "def plus")
inductive myNat where
| zero : myNat
| succ (n : myNat) : myNat
def my1 := myNat.succ myNat.zero
def my43 := match my1 with
| myNat.zero => 42
| myNat.succ _ => 43
def myIncomplete := match my1 with
| myNat.zero => 42
#####
#
# inductive-Option
# 2024may15
#
#####
# «inductive-Option» (to ".inductive-Option")
# (find-fplean4page 40 "inductive Option")
# (find-fplean4text 40 "inductive Option")
# (find-fplean4page 40 "def List.head?")
# (find-fplean4text 40 "def List.head?")
#####
#
# inductive-Syntax
# 2024may15
#
#####
# «inductive-Syntax» (to ".inductive-Syntax")
# (find-lean-links "Syntax")
# (find-leanmetadocrfile "main/01_intro.lean" "Concrete Syntax Tree, Lean's `Syntax` type")
# (find-leanmetadocrgrep "grep --color=auto -nRH --null -e 'Syntax' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'Syntax' *")
# (find-lean4pregrep "grep --color=auto -nRHw --null -e 'Syntax' *")
# (find-lean4prefile "Lean/Syntax.lean")
# (find-lean4prefile "Init/Prelude.lean" "inductive Syntax where")
# (find-lean4prefile "Init/Prelude.lean" "inductive SourceInfo where")
# (find-leanmetadoc "extra/03_pretty-printing")
# (find-leanmetadoc "main/04_metam#exercises" "let stx : Syntax")
# (find-leanmetadocr "main/04_metam#exercises" "let stx : Syntax")
# (find-leanmetadoc "main/05_syntax")
# (find-leanmetadoc "main/05_syntax#operating-on-syntax")
# (find-leanmetadocr "main/05_syntax" "## Operating on Syntax")
# (find-leanmetadoc "main/05_syntax#matching-on-syntax")
# (find-leanmetadocr "main/05_syntax" "### Matching on `Syntax`")
/home/edrx/usrc/lean4-metaprogramming-book/lean/main/05_syntax.lean
file:///home/edrx/snarf/https/leanprover-community.github.io/lean4-metaprogramming-book/md/main/04_metam.html#exercises
#####
#
# 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")
#####
#
# interpolatedStr
# 2024may16
#
#####
# «interpolatedStr» (to ".interpolatedStr")
# (to "string-interpolation")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 's!' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'interpolatedStr' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'syntax:max \"s!\"' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'syntax:max \"m!\"' *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'syntax:max \"f!\"' *")
# (find-lean4prefile "Lean/Parser/StrInterpolation.lean")
# (find-lean4prefile "Init/Data/ToString/Macro.lean" "syntax:max \"s!\"")
# (find-lean4prefile "Lean/Message.lean" "syntax:max \"m!\"")
# (find-lean4prefile "Init/Data/Format/Macro.lean" "syntax:max \"f!\"")
#####
#
# 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
#####
#
# latin-cross
# 2024apr20
#
#####
# «latin-cross» (to ".latin-cross")
# (find-lean-links "✝")
# (find-lean4pregrep "grep --color=auto -nRH --null -e '✝' *")
# (find-lean4prefile "Init/Meta.lean" "s.contains '✝' || s == \"_inaccessible\"")
#####
#
# leading_parser
# 2024mar27
#
#####
# «leading_parser» (to ".leading_parser")
# (find-lean-links "leading_parser")
# (find-lean4grep "grep --color=auto -nRH --null -e 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/Elab/BuiltinNotation.lean" "@[builtin_term_elab «leading_parser»]")
# (find-lean4prefile "Lean/Parser/Syntax.lean" "def «precedence» := leading_parser")
# (find-lean4prefile "Lean/Parser/Term.lean" "def «fun» := leading_parser:maxPrec")
# https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Leading.20parser/near/431690866 yz, 2024apr06
# https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/leading_parser.3F/near/438403571 me, 2024may13
Kyle Miller: Usually it's
">> becomes space and f x y z becomes f(x, y, z)"
though sometimes the parser name for syntax can be a little different.
There are also transformations like many p becomes p* and many1 p
becomes p+, among some others.
#####
#
# Mário Carneiro: The Type Theory of Lean
# 2024may07
#
#####
# «lean-type-theory» (to ".lean-type-theory")
# (find-angg ".emacs.papers" "leanttmain")
# (find-angg ".emacs.papers" "leanttslides")
# https://github.com/digama0/lean-type-theory
# 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
# (find-youtubedl-links "/sda5/videos/" nil "3sKrSNhSxik" nil "{stem}")
# (find-youtubedl-links "/sda5/videos/" "The_Type_Theory_of_Lean" "3sKrSNhSxik" ".mkv" "leantt")
# (code-video "leanttvideo" "/sda5/videos/The_Type_Theory_of_Lean-3sKrSNhSxik.mkv")
# (find-leanttvideo "0:00")
# (find-git-links "https://github.com/digama0/lean-type-theory" "leantt")
# (code-c-d "leantt" "~/usrc/lean-type-theory/")
# (find-leanttfile "")
(code-pdf-page "leanttmain" "$S/https/github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf")
(code-pdf-text8 "leanttmain" "$S/https/github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf")
;; (find-leanttmainpage)
;; (find-leanttmaintext)
;; (find-leanttmainpage 8 "2.5 Definitions")
;; (find-leanttmaintext 8 "2.5 Definitions")
;; (find-leanttmainpage 9 "telescope")
;; (find-leanttmaintext 9 "telescope")
(code-pdf-page "leanttslides" "$S/https/github.com/digama0/lean-type-theory/releases/download/v1.0/slides.pdf")
(code-pdf-text8 "leanttslides" "$S/https/github.com/digama0/lean-type-theory/releases/download/v1.0/slides.pdf")
;; (find-leanttslidespage)
;; (find-leanttslidestext)
#####
#
# 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")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'match \"' *")
#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
#####
#
# minted
# 2024apr28
#
#####
# «minted» (to ".minted")
# https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html
# (find-lean4doc "syntax_highlight_in_latex")
# (find-esgrep "grep --color=auto -nH --null -e minted *.e")
#####
#
# 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>")
# (find-lean4prefile "Lean/Elab/BuiltinTerm.lean" "@[builtin_term_elab «open»]")
#####
#
# 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")
#####
#
# <|>, a.k.a. orelse
# 2024may15
#
#####
# «orelse» (to ".orelse")
# (find-lean4prefile "Init/Notation.lean" "`p1 <|> p2` is shorthand for `orelse(p1, p2)`")
# (find-lean4prefile "Init/Notation.lean" "`(stx| $p₁ <|> $p₂) => `(stx| orelse($p₁, $p₂))")
#####
#
# 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 "structure")
# (to "instance")
# (find-fplean4page 19 "deriving Repr")
# (find-fplean4text 19 "deriving Repr")
# (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")
#####
#
# scoped-syntax
# 2024may15
#
#####
# «scoped-syntax» (to ".scoped-syntax")
# (to "check")
# (find-leanmetadoc "main/05_syntax#free-form-syntax-declarations")
# (find-leanmetadocw "main/05_syntax#free-form-syntax-declarations")
# (find-leanmetadocr "main/05_syntax" "### Free form syntax declarations")
# (find-leanmetadocr "main/05_syntax" "namespace Playground2")
# (find-lean4prefile "Lean/Elab/Term.lean" "elaboration function for '{k}' has not been implemented")
# (find-lean4prefile "Lean/Elab/Command.lean" "elaboration function for '{k}' has not been implemented")
#####
#
# show
# 2024mar22
#
#####
# «show» (to ".show")
# (find-lean-links "show")
# (find-tpinlean4file "propositions_and_proofs.md" "show p from hp")
# (find-tpinlean4page 25 "show p from hp")
# (find-tpinlean4text 25 "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")
variable {P : Prop}
variable {Q : Prop}
theorem t1 : P → Q → P :=
fun p : P =>
fun q : Q =>
show P from p
theorem t1 : P → Q → P := fun p : P => fun q : Q => show P from p
theorem t0 : P → P := fun p : P => show P from p
theorem t0a : P → P := fun p : P => show P from p
theorem t0b : P → P := fun p : P => p
#check fun p : P => show P from p
#check show Int from 42
#check fun p : P => show P from p
#check fun p : P => p
#check show Int from 42
#####
#
# s!"str" and m!"str"
# 2024mar23
#
#####
# «string-interpolation» (to ".string-interpolation")
# (to "interpolatedStr")
# (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")
#####
#
# structures
# 2023jun24
#
#####
# «structure» (to ".structure")
# «structures» (to ".structures")
# (to "Repr")
# (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
def p45 : Point := { x := 4, y := 5 }
#eval p45
#eval { p45 with y := 6 }
#check Point.mk
#check Point.x
#check Point.y
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}
#####
#
# tagged-subgoals
# 2024apr30
#
#####
# «tagged-subgoals» (to ".tagged-subgoals")
# (find-angg ".emacs.papers" "tpinlean4" "57" "tagged the first subgoal as left")
variable (P Q R : Prop)
variable {P Q R : Prop}
variable {p : P}
variable {q : Q}
example (p : P) (q : Q) : P ∧ Q := And.intro p q
#check fun (p : P) (q : Q) => And.intro p q
#####
#
# telescopes
# 2024apr27
#
#####
# «telescopes» (to ".telescopes")
# (find-angg "LEAN/telescopes1.lean")
#####
#
# termParser
# 2024may15
#
#####
# «termParser» (to ".termParser")
# (find-lean4prefile "Lean/Parser/Basic.lean" "def termParser")
# (find-lean4prefile "Lean/Parser/Basic.lean" "def categoryParser")
#####
#
# 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»")
variable (P Q R : Prop)
variable {P Q R : Prop}
theorem t1a : P → P := fun p : P => p
theorem t1b : P → P := fun p : P => show P from p
theorem t1c (p : P) : P := p
#print t1a -- p → q → p
#print t1b -- p → q → p
#print t1c -- p → q → p
theorem ta (p : P) (q : Q) : P ∧ Q := And.intro p q
example (p : P) (q : Q) : P ∧ Q := And.intro p q
#check fun (p : P) (q : Q) => And.intro p q
#check fun (p : P) (q : Q) =>
let paq := And.intro p q
paq
#####
#
# toolchains
# 2024may12
#
#####
# «toolchains» (to ".toolchains")
# (find-fline "~/.elan/toolchains/")
#####
#
# try-catch
# 2024may12
#
#####
# «try-catch» (to ".try-catch")
# (find-leanmetadoc "main/01_intro#building-a-command")
# (find-leanmetadocr "main/01_intro" "### Building a command")
# (find-lean4prefile "Lean/CoreM.lean" "try-catch")
# (find-lean4prefile "Lean/Elab/Do.lean" "def doTry :=")
# (find-lean4pregrep "grep --color=auto -nRH --null -e catch *")
# (find-lean4pregrep "grep --color=auto -nRH --null -e 'catch \"' *")
#####
#
# typeof
# 2024may05
#
#####
# «typeof» (to ".typeof")
# (find-lean-links "typeof")
# (find-lean4pregrep "grep --color=auto -niRH --null -e 'typeof' *")
def foo1 {A : _} (a : A) := a
def foo2 {A : _} (_ : A) := A
#check foo1 42
#check foo2 42
#####
#
# 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 _")
# (find-tpinlean4page 87 "unicode brackets")
# (find-tpinlean4text 87 "unicode brackets")
# (find-lean4grep "grep --color=auto -nRH --null -e 'synthesize placeholder' *")
# (find-lean4file "src/Lean/Elab/Term.lean" "synthesize placeholder")
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/01_intro#building-a-command")
# (find-leanmetadocr "main/01_intro#building-a-command")
# (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")
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")
https://github.com/kmill
https://github.com/kmill/lean4-raytracer
https://github.com/kmill/LeanTeX
https://github.com/kmill/glimpse_of_lean
https://github.com/kmill/leanprover-community.github.io
https://github.com/kmill/tutorials
https://leanprover-community.github.io/archive/stream/270676-lean4/topic/getting.20started.20with.20Lean.204.html
https://kmill.github.io/cv/cv.pdf
# Local Variables:
# coding: utf-8-unix
# End: