Lean 4 (Meta)programming Cookbook

Index🔗

Symbols

  1. "Hello World" Command

A

  1. ANSI Colors
  2. Adding Syntax for terms
  3. Adding syntax (categories)
  4. Adding syntax for commands
  5. Advanced HashMap Operations
  6. Appending to a file
  7. Async Sleep
  8. add
    1. Nat.add

B

  1. Binary Search Tree

C

  1. Check File Size
  2. Checking Metadata for Path
  3. Checking Tactics
  4. Checking if Path is Absolute or Relative
  5. Code, Syntax, and Expressions
  6. Command for checking whether a proposition is solved by grind
  7. Concatenating file paths
  8. Converting JSON to TOML
  9. Converting TOML to JSON
  10. Creating directories

D

  1. DSL for HTML unordered lists
  2. Deadlocking the Task System
  3. Declaring a syntax category
  4. Defining Binary Tree
  5. Deleting a directory
  6. Deleting a file
  7. Displaying in the Infoview

E

  1. Encoding TOML
  2. Environment Extensions and Attributes
  3. Environment Extensions and Attributes: Example
  4. Expressions for (dependent) Functions and Function-types
  5. Expressions from Function Applications

F

  1. File Compression and Decompression

G

  1. Get PID of a Process
  2. Get Thread IDs
  3. Get a Random Number
  4. 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. IO.asTask and BaseIO.asTask
  3. Interruptible Sleep

J

  1. Json Field Renaming
  2. Json Handling Default Values

L

  1. List to Binary Tree
  2. Listing contents of a directory
  3. log­Error
  4. log­Info
  5. log­Warning

M

  1. Memoization using HashMap
  2. Modifying Goals
  3. Modifying JSON objects
  4. Modifying TOML objects
  5. Monads in Practise
  6. Mutable Variables across commands
  7. Mutable Variables: Example

N

  1. Nat.add

O

  1. Operations on Binary Tree
  2. Overwriting CLI lines

P

  1. Parsing Command Line Arguments
  2. Parsing TOML
  3. Parsing lakefile.toml
  4. Pattern-matching expressions by solving
  5. Pattern-matching expressions directly
  6. Printing to Stdout and Stderr
  7. Process Idle Sleep
  8. Progress Bars and Spinners
  9. Putting a Process to Sleep
  10. Python exponentiation DSL
  11. Python for loop DSL

Q

  1. Quasi-Quotes: Creating and Matching Syntax

R

  1. RBMap Operations
  2. RBTree Basic Operations
  3. Read and Set File Permissions
  4. Reading Environment Variables
  5. Reading JSONL files
  6. Reading Nested TOML
  7. Reading TOML files
  8. Reading a JSON file
  9. Reading from Stdin
  10. Reading from a file
  11. Reading values from JSON
  12. Reading values from TOML
  13. Recursive directory traversal
  14. Renaming a File Path
  15. Replacing with What Works
  16. Running Tasks in Parallel

S

  1. Scheduling Processes with RBMap
  2. Setting Environment Variables for Child Process
  3. Setting File Permissions
  4. Spawning Tasks and Worker Threads
  5. Spawning a Child Process
  6. State Monad: Remembering Computations

T

  1. Tactic to print the main goal
  2. Tactic to prove natural number inequalities
  3. Tactic to repeat applications of theorems
  4. Tactics as shortcuts
  5. Terminating a Process
  6. Timing performance
  7. Tracking Undefined Identifiers with RBTree
  8. Types of Expressions

U

  1. Updating lakefile.toml

V

  1. Viewing and Closing Goals

W

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