diff --git a/.github/workflows/blank.yml b/.github/workflows/blank.yml
new file mode 100644
index 0000000..8d215ca
--- /dev/null
+++ b/.github/workflows/blank.yml
@@ -0,0 +1,36 @@
+# This is a basic workflow to help you get started with Actions
+
+name: CI
+
+# Controls when the workflow will run
+on:
+ # Triggers the workflow on push or pull request events but only for the "main" branch
+ push:
+ branches: [ "cadake" ]
+ pull_request:
+ branches: [ "cadake" ]
+
+ # Allows you to run this workflow manually from the Actions tab
+ workflow_dispatch:
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+ # This workflow contains a single job called "build"
+ build:
+ # The type of runner that the job will run on
+ runs-on: ubuntu-latest
+
+ # Steps represent a sequence of tasks that will be executed as part of the job
+ steps:
+ # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
+ - uses: actions/checkout@v4
+
+ # Runs a single command using the runners shell
+ - name: Run a one-line script
+ run: echo Hello, world!
+
+ # Runs a set of commands using the runners shell
+ - name: Run a multi-line script
+ run: |
+ echo Add other actions to build,
+ echo test, and deploy your project.
diff --git a/Chap1.qmd b/Chap1.qmd
index 90987d1..ba4e927 100644
--- a/Chap1.qmd
+++ b/Chap1.qmd
@@ -1,36 +1,37 @@
# Sentential Logic
+
\markdouble{1 Sentential Logic}
Chapter 1 of *How To Prove It* introduces the following symbols of logic:
::: {style="margin: 0% 20%"}
-| Symbol | Meaning |
-|:------:|:-------:|
-| $\neg$ | not |
-| $\wedge$ | and |
-| $\vee$ | or |
-| $\to$ | if ... then |
+| Symbol | Meaning |
+|:-----------------:|:-----------------------------:|
+| $\neg$ | not |
+| $\wedge$ | and |
+| $\vee$ | or |
+| $\to$ | if ... then |
| $\leftrightarrow$ | iff (that is, if and only if) |
:::
-As we will see, Lean uses the same symbols, with the same meanings. A statement of the form $P \wedge Q$ is called a *conjunction*, a statement of the form $P \vee Q$ is called a *disjunction*, a statement of the form $P \to Q$ is an *implication* or a *conditional* statement (with *antecedent* $P$ and *consequent* $Q$), and a statement of the form $P \leftrightarrow Q$ is a *biconditional* statement. The statement $\neg P$ is the *negation* of $P$.
+As we will see, Lean uses the same symbols, with the same meanings. A statement of the form $P \wedge Q$ is called a *conjunction*, a statement of the form $P \vee Q$ is called a *disjunction*, a statement of the form $P \to Q$ is an *implication* or a *conditional* statement (with *antecedent* $P$ and *consequent* $Q$), and a statement of the form $P \leftrightarrow Q$ is a *biconditional* statement. The statement $\neg P$ is the *negation* of $P$.
This chapter also establishes a number of logical equivalences that will be useful to us later:
-::: {id="prop-laws"}
-| Name | | Equivalence | |
-|:---------|:-----:|:-----:|:-----:|
+::: {#prop-laws}
+| Name | | Equivalence | |
+|:---------------------|:---------------:|:---------------:|:---------------:|
| De Morgan's Laws | $\neg (P \wedge Q)$ | is equivalent to | $\neg P \vee \neg Q$ |
-| | $\neg (P \vee Q)$ | is equivalent to | $\neg P \wedge \neg Q$ |
+| | $\neg (P \vee Q)$ | is equivalent to | $\neg P \wedge \neg Q$ |
| Double Negation Law | $\neg\neg P$ | is equivalent to | $P$ |
| Conditional Laws | $P \to Q$ | is equivalent to | $\neg P \vee Q$ |
-| | $P \to Q$ | is equivalent to | $\neg(P \wedge \neg Q)$ |
+| | $P \to Q$ | is equivalent to | $\neg(P \wedge \neg Q)$ |
| Contrapositive Law | $P \to Q$ | is equivalent to | $\neg Q \to \neg P$ |
:::
-Finally, Chapter 1 of *HTPI* introduces some concepts from set theory. A *set* is a collection of objects; the objects in the collection are called *elements* of the set. The notation $x \in A$ means that $x$ is an element of $A$. Two sets $A$ and $B$ are equal if they have exactly the same elements. We say that $A$ is a *subset* of $B$, denoted $A \subseteq B$, if every element of $A$ is an element of $B$. If $P(x)$ is a statement about $x$, then $\{x \mid P(x)\}$ denotes the set whose elements are the objects $x$ for which $P(x)$ is true. And we have the following operations on sets:
+Finally, Chapter 1 of *HTPI* introduces some concepts from set theory. A *set* is a collection of objects; the objects in the collection are called *elements* of the set. The notation $x \in A$ means that $x$ is an element of $A$. Two sets $A$ and $B$ are equal if they have exactly the same elements. We say that $A$ is a *subset* of $B$, denoted $A \subseteq B$, if every element of $A$ is an element of $B$. If $P(x)$ is a statement about $x$, then $\{x \mid P(x)\}$ denotes the set whose elements are the objects $x$ for which $P(x)$ is true. And we have the following operations on sets:
-::: {.quote}
+::: quote
$A \cap B = \{x \mid x \in A \wedge x \in B\} = {}$ the *intersection* of $A$ and $B$,
$A \cup B = \{x \mid x \in A \vee x \in B\} = {}$ the *union* of $A$ and $B$,
diff --git a/docs/Chap1.html b/docs/Chap1.html
index 6ec40d9..6dccde7 100644
--- a/docs/Chap1.html
+++ b/docs/Chap1.html
@@ -2,12 +2,12 @@
-
+
-How To Prove It With Lean - 1 Sentential Logic
+1 Sentential Logic – How To Prove It With Lean
@@ -47,7 +47,13 @@
"collapse-after": 3,
"panel-placement": "start",
"type": "textbox",
- "limit": 20,
+ "limit": 50,
+ "keyboard-shortcut": [
+ "f",
+ "/",
+ "s"
+ ],
+ "show-item-context": false,
"language": {
"search-no-results-text": "No results",
"search-matching-documents-text": "matching documents",
@@ -56,13 +62,43 @@
"search-more-match-text": "more match in this document",
"search-more-matches-text": "more matches in this document",
"search-clear-button-title": "Clear",
+ "search-text-placeholder": "",
"search-detached-cancel-button-title": "Cancel",
- "search-submit-button-title": "Submit"
+ "search-submit-button-title": "Submit",
+ "search-label": "Search"
}
}
+
+
+
@@ -70,11 +106,16 @@
-