CONTENTS 1 Using Lean 1 1.1 Using Lean Online 1 1.2 Using Lean with VSCode 1 1.3 Using Lean with Emacs 2 1.4 Using the Package Manager 3 2 Lexical Structure 7 2.1 Symbols and Commands 7 2.2 Identifiers to open the root directory for the project. ### 1.3 Using Lean with Emacs Assuming you have installed Lean, Emacs, and the Lean Emacs mode according to the instructions on the Lean Download page, you simply simply need to create a file with the extension .lean and edit it in Emacs. The file will be checked continuously as you type. For example, if you type the words #check id, the word #check is underlined

Automatic Proof Search (Auto) ..... 93 4.2 Command-line options ..... 96 4.3 Compilers ..... 99 4.4 Emacs Mode ..... 101 4.5 Literate Programming ..... 105 4.6 Generating HTML ..... 106 4.7 Generating Ubuntu from Karmic onwards. To install: apt-get install agda-mode This should install Agda and the Emacs mode. The standard library is available in Debian testing/unstable and Ubuntu from Lucid onwards Agda will pull in emacs-agda-mode and ghc-Agda-devel. ## NixOS Agda is part of the Nixpkgs collection that is used by http://nixos.org/nixos. To install Agda and agda-mode for Emacs, type: nix-env -f

of the tokens print axioms : display assumed axioms print options : display options set by user or emacs mode print prefix : display all declarations in the namespace print coercions : display : execute a single tactic with different options ( is a comma-separated list) ## Emacs Lean-mode commands ## Flycheck commandsEmacs Lean mode. ## Logical symbols |Unicode|Ascii|Emacs| |---|---|---| |true||| |false||| |¬|not|\\not, \\neg| |^|/\\\\|\\and|

Proof Search (Auto) ..... 141 4.2 Command-line options ..... 144 4.3 Compilers ..... 150 4.4 Emacs Mode ..... 152 4.5 Literate Programming ..... 157 4.6 Generating HTML ..... 159 4.7 Generating Alex: https://www.haskell.org/alex/ • Happy: https://www.haskell.org/happy/ • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your your shell’s search path. For instructions on installing a suitable version of Emacs under Windows, see Installing Emacs under Windows. Non-Windows users need to ensure that the development files for the

o Without K ## • Tools • Automatic Proof Search (Auto) Command-line options Compilers ○ Emacs Mode • Literate Programming Generating HTML Generating LaTeX Library Management • Contribute system can be used can be found in chapter Tools. ## Getting Started • Prerequisites Installing Emacs under Windows • Installation Installation from Hackage ○ Prebuilt Packages and System-Specific Alex: https://www.haskell.org/alex/ • Happy: https://www.haskell.org/happy/ • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your

o Without K ## • Tools • Automatic Proof Search (Auto) Command-line options Compilers ○ Emacs Mode • Literate Programming Generating HTML Generating LaTeX Library Management • Contribute system can be used can be found in chapter Tools. ## Getting Started • Prerequisites Installing Emacs under Windows • Installation Installation from Hackage ○ Prebuilt Packages and System-Specific https://www.haskell.org/happy/ • cpphs: https://hackage.haskell.org/package/cpphs • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your

o Without K ## • Tools • Automatic Proof Search (Auto) Command-line options Compilers ○ Emacs Mode • Literate Programming Generating HTML Generating LaTeX Library Management • Contribute system can be used can be found in chapter Tools. ## Getting Started • Prerequisites Installing Emacs under Windows • Installation Installation from Hackage ○ Prebuilt Packages and System-Specific https://www.haskell.org/happy/ • cpphs: https://hackage.haskell.org/package/cpphs • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your

4.1 Automatic Proof Search (Auto) 111 4.2 Command-line options 114 4.3 Compilers 118 4.4 Emacs Mode 120 4.5 Literate Programming 125 4.6 Generating HTML 127 4.7 Generating LaTeX 127 4.8 https://www.haskell.org/happy/ • cpphs: https://hackage.haskell.org/package/cpphs • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your your shell’s search path. For instructions on installing a suitable version of Emacs under Windows, see Installing Emacs under Windows. Non-Windows users need to ensure that the development files for the

4.1 Automatic Proof Search (Auto) 111 4.2 Command-line options 114 4.3 Compilers 118 4.4 Emacs Mode 120 4.5 Literate Programming 125 4.6 Generating HTML 127 4.7 Generating LaTeX 127 4.8 https://www.haskell.org/happy/ • cpphs: https://hackage.haskell.org/package/cpphs • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your your shell’s search path. For instructions on installing a suitable version of Emacs under Windows, see Installing Emacs under Windows. Non-Windows users need to ensure that the development files for the

4.1 Automatic Proof Search (Auto) 111 4.2 Command-line options 114 4.3 Compilers 118 4.4 Emacs Mode 120 4.5 Literate Programming 125 4.6 Generating HTML 127 4.7 Generating LaTeX 127 4.8 Alex: https://www.haskell.org/alex/ • Happy: https://www.haskell.org/happy/ • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your shell's search path. For instructions on installing a suitable version of Emacs under Windows, see Installing Emacs under Windows. Non-Windows users need to ensure that the development files for