cheat sheet

jsiek · Oct 23, 2024 · d3549d8 · d3549d8
1 parent 7f24b3a
commit d3549d8
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/doc/CheatSheet.md b/doc/CheatSheet.md
@@ -0,0 +1,6 @@
+
+
+| Formula    |  Prove        | Use      |
+| ---------- | ------------- | -------- |
+| `P and Q`  |  `,` [Comma](./Reference.md#comma-conjunction-and-introduction)) | (1) implicit as `P` (2) implicit as `Q` |
+| `P or Q`   | (1) implicit from `P` (2) implicit from `Q` | 
diff --git a/ex/Sum.pf b/ex/Sum.pf
@@ -90,4 +90,4 @@ proof
         = summation(length(xs), 0, nth(xs,0)) + summation(length(ys), 0, nth(ys,0))
       by apply summation_add[length(xs)][length(ys), 0, 0, nth(xs ++ ys, 0), nth(xs,0), nth(ys,0)]
          to p1, p2
-end
+end