From 85e6c26953ffa2555edf42cc9191a6a9fcab45ad Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Mon, 24 Feb 2025 11:50:24 -0500 Subject: [PATCH] vault backup: 2025-02-24 11:50:24 --- 3-99 Research/Assembly/Assembly - README.md | 3 +-- 3-99 Research/LEAN/LEAN - README.md | 16 +--------------- 3-99 Research/LEAN/Tutorial World.md | 10 ++++++---- 3-99 Research/TLA/TLA - README.md | 2 +- 5 Thesis/1 Ideas/1 Ideas - README.md | 3 +-- 5 files changed, 10 insertions(+), 24 deletions(-) diff --git a/3-99 Research/Assembly/Assembly - README.md b/3-99 Research/Assembly/Assembly - README.md index 96e1dadeb..9efce398b 100644 --- a/3-99 Research/Assembly/Assembly - README.md +++ b/3-99 Research/Assembly/Assembly - README.md @@ -2,9 +2,8 @@ ## Files - [[Assembly Canvas.canvas]] -- [[3-99 Research/Assembly/Untitled]] +- [[Untitled.md]] ## Summary - Generated by llama3.2:latest diff --git a/3-99 Research/LEAN/LEAN - README.md b/3-99 Research/LEAN/LEAN - README.md index 971d63481..5cee6af07 100644 --- a/3-99 Research/LEAN/LEAN - README.md +++ b/3-99 Research/LEAN/LEAN - README.md @@ -2,22 +2,8 @@ ## Files - [[Learning Plan.md]] +- [[Tutorial World.md]] ## Summary -Here is the Markdown description of what's inside the folder: - -# LEAN Folder Contents - -This folder contains notes and resources related to [LEAN](https://en.wikipedia.org/wiki/Lean_management), a management philosophy focused on eliminating waste and optimizing processes. - -The contents include: - -- A [[Learning Plan.md]] outlining my approach to learning about LEAN -- Various research documents, including: - - [Tutorial World #LEAN](https://example.com) for February 2025 - - [Addition World #LEAN](https://example.com) for February 2025 - - [Implication World #LEAN](https://example.com) for March 2025 - - [Multiplication World #LEAN](https://example.com) for March 2025 - - [Schedule further worlds #LEAN](https://example.com) for March 2025 Generated by llama3.2:latest diff --git a/3-99 Research/LEAN/Tutorial World.md b/3-99 Research/LEAN/Tutorial World.md index 8696570a2..943fdc7e3 100644 --- a/3-99 Research/LEAN/Tutorial World.md +++ b/3-99 Research/LEAN/Tutorial World.md @@ -1,5 +1,7 @@ # Tactics -| Tactic Name | Ex. Expr. | What does it do? | -| ----------- | --------- | ----------------------------------------- | -| `rfl` | $X = X$ | Proves all theorems of the observed form. | -| `rw` | | | +| Tactic Name | Ex. Expr. | What does it do? | +| ----------- | ------------ | ------------------------------------------------------------- | +| `rfl` | $X = X$ | Proves all theorems of the observed form. | +| `rw [h]` | $Y = X+a$ | 'Rewrite' an equation using an assumption 'h' or similar. | +| `succ x` | $Y = Y+1$ | 'Successor' says that some number is bigger than another one. | +| `\l` | $\leftarrow$ | Does the opposite of rw. Turns Ys into Xs | diff --git a/3-99 Research/TLA/TLA - README.md b/3-99 Research/TLA/TLA - README.md index 4890268f8..2625278eb 100644 --- a/3-99 Research/TLA/TLA - README.md +++ b/3-99 Research/TLA/TLA - README.md @@ -3,7 +3,7 @@ ## Files - [[TLA Canvas.canvas]] - [[TLA+ Learning Plan.md]] -- [[3-99 Research/TLA/Untitled]] +- [[Untitled.md]] - [[What is TLA?.md]] - [[What the hell is liveness?.md]] diff --git a/5 Thesis/1 Ideas/1 Ideas - README.md b/5 Thesis/1 Ideas/1 Ideas - README.md index d065e7fce..5a715cb42 100644 --- a/5 Thesis/1 Ideas/1 Ideas - README.md +++ b/5 Thesis/1 Ideas/1 Ideas - README.md @@ -1,9 +1,8 @@ # Table of Contents for 1 Ideas ## Files -- [[5 Thesis/1 Ideas/Untitled]] +- [[Untitled.md]] ## Summary - Generated by llama3.2:latest