Lean 4 (Meta)programming Cookbook

Index🔗

A

  1. ANSI Colors
  2. Adding Term Syntax
  3. Adding syntax (categories)
  4. Advanced HashMap Operations
  5. Appending to a file
  6. Attributes for commands

B

  1. Building expressions with variables, functions, and dependent function types

C

  1. Check File Size
  2. Checking Metadata for Path
  3. Checking if Path is Absolute or Relative
  4. Checking validity of Tactics
  5. Code, Syntax, and Expressions
  6. Concatenating file paths
  7. Converting JSON to TOML
  8. Converting TOML to JSON
  9. Creating directories

D

  1. Deleting a directory
  2. Deleting a file
  3. Displaying in the Infoview

E

  1. Encoding TOML
  2. Environment Extensions
  3. Exact Pattern-Matching
  4. Expressions for function applications
  5. elaborating terms, commands and tactics

F

  1. File Compression and Decompression

G

  1. Get a Random Number
  2. Getting Current Working Directory

H

  1. Handling JSON files
  2. Handling JSONL files
  3. Handling Json Object
  4. Handling Nested TOML
  5. HashMap Basic Operations
  6. Hello World Tactic
  7. How to build a Recipe

I

  1. I/O and Processes
  2. Introducing commands

J

  1. Json Field Renaming
  2. Json Handling Default Values

L

  1. Listing contents of a directory

M

  1. Memoization using HashMap
  2. Modifying JSON objects
  3. Modifying TOML objects
  4. Monads in Practise

O

  1. Overwriting CLI lines

P

  1. Parallel IO
  2. Parsing Command Line Arguments
  3. Parsing TOML
  4. Parsing lakefile.toml
  5. Pattern-matching by solving
  6. Printing to Stdout and Stderr
  7. Progress Bars and Spinners
  8. Putting a Process to Sleep

Q

  1. Quasi-Quotes: Creating and Matching Syntax

R

  1. RBMap Operations
  2. RBTree Basic Operations
  3. Reading Environment Variables
  4. Reading JSONL files
  5. Reading Nested TOML
  6. Reading TOML files
  7. Reading a JSON file
  8. Reading from Stdin
  9. Reading from a file
  10. Reading values from JSON
  11. Reading values from TOML
  12. Recursive directory traversal
  13. Renaming a File Path
  14. Replacing code using Try­This
  15. Running an external program

S

  1. Scheduling Processes with RBMap
  2. Setting Environment Variables for Child Process
  3. State monads
  4. State using IO.Ref
  5. Syntax strings from expressions

T

  1. Tactic using macros
  2. Tactics as abbreviations and mnemonics
  3. Tactics close goals
  4. Tactics giving new goals.
  5. Tactics using elaborators
  6. Tasks and Concurrency
  7. Timing performance
  8. Tracking Undefined Identifiers with RBTree
  9. Types of Expressions
  10. trying different natural numbers

U

  1. Updating lakefile.toml

W

  1. Walking a directory tree
  2. Writing JSONL files
  3. Writing TOML files
  4. Writing to JSON files
  5. Writing to a file