(Re)generate: (find-lean4-intro)
Source code:  (find-efunction 'find-lean4-intro)
More intros:  (find-eev-quick-intro)
              (find-eev-intro)
              (find-eepitch-intro)
This buffer is _temporary_ and _editable_.
It is meant as both a tutorial and a sandbox.


THIS IS A WORK IN PROGRESS!
THIS IS A VERY EARLY DRAFT!

Test this page in HTML first:
  http://anggtwu.net/eev-intros/find-lean4-intro.html

  (find-lean4doc     "whatIsLean")
  (find-leantpildoc  "introduction")
  (find-fplean4doc   "getting-to-know/evaluating")
  (find-leanmetadoc  "main/01_intro")
  (find-leanmathsdoc "index")
  (find-leanrefdocw  "using_lean#using-lean-with-emacs")

https://leanprover-community.github.io/install/debian.html
https://leanprover-community.github.io/install/debian_details.html

(find-es "lean" "lean4-mode")

Prerequisites:
  (find-rstdoc-intro)
  (find-angg ".emacs.lean.el")
  (find-angg-es-links)
  (find-windows-beginner-intro "7. Test Maxima with find-wget")


. `find-wgetrecursive-links'
  (find-wgetrecursive-links "https://lean-lang.org/lean4/doc/")
  (find-wgetrecursive-links "https://lean-lang.org/theorem_proving_in_lean4/")
  (find-wgetrecursive-links "https://lean-lang.org/functional_programming_in_lean/")
  (find-wgetrecursive-links "https://leanprover-community.github.io/lean4-metaprogramming-book/")
  (find-wgetrecursive-links "https://leanprover-community.github.io/mathematics_in_lean/")
  (find-wgetrecursive-links "https://leanprover.github.io/reference/")