Warning: this is an htmlized version!
The original is across this link,
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.
#
# 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/>.
#
#######



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




#  Local Variables:
#  coding:               raw-text-unix
#  ee-delimiter-hash:    "\n#*\n"
#  ee-delimiter-percent: "\n%*\n"
#  ee-anchor-format:     "«%s»"
#  End: