Update doc/note/facts.md for facts vs truths
diff --git a/doc/note/facts.md b/doc/note/facts.md
index 07f2a37..65d8e9a 100644
--- a/doc/note/facts.md
+++ b/doc/note/facts.md
@@ -54,15 +54,21 @@
## Creating Facts
-One way to create a fact is by assignment. Immediately after the statement `a =
-rhs`, the boolean expression `a == rhs` is a true fact, provided that `rhs` is
-an expression with no [side effects](/doc/note/effects.md). That assignment
-also either removes or updates any other fact involving `a`.
+Every fact is true (at its point in the program), but not every truth is a
+fact. For example, if `x < 5` is true then `x < 6`, `x < 7`, `x < 8`, etc are
+an infinite sequence of truths, but the Wuffs tools only track a finite number
+of facts at any given point. Some facts are explicitly created and some facts
+are implicitly created. But all facts are created by specific means.
+
+One way to implicitly create a fact is by assignment. Immediately after the
+statement `a = rhs`, the boolean expression `a == rhs` is a true fact, provided
+that `rhs` is an expression with no [side effects](/doc/note/effects.md). That
+assignment also either removes or updates any other fact involving `a`.
TODO: specify exactly when and how facts are removed or updated.
-As alluded to above, another way to create a fact is to explicitly check if it
-is true, using an `if` or `while` statement:
+As alluded to above, another way to implicitly create a fact is to explicitly
+check if it is true, using an `if` or `while` statement:
```
// "x < (y + z)" isn't necessarily true here...
@@ -85,8 +91,8 @@
}
```
-Facts are also created by compile-time [assertions](/doc/note/assertions.md),
-discussed in a separate document.
+Facts are also explicitly created by compile-time
+[assertions](/doc/note/assertions.md), discussed in a separate document.
## Situations and Reconciliation
