Tweak docs

docs/src/content/docs/docs/api/dusasolution.md

@@ -5,39 +5,39 @@ title: class DusaSolution
 A `DusaSolution` is a queryable solution to a Dusa program returned by
 [solving a `Dusa` instance](docs/api/dusa/#solving-a-dusa-instance).
 
-## `facts` getter
+## Checking facts
 
-The `facts` getter provides an iterator over all the [facts](/docs/api/terms/#fact)
-in a solution.
+### `has()`method
 
-```javascript
-const dusa = new Dusa(`
-    #builtin INT_MINUS minus
-    digit 9.
-    digit (minus N 1) :- digit N, N != 0.`);
+The `has()` method is intended to check whether a relational proposition
+exists in a solution.
 
-for (const fact of dusa.solution.facts) {
-  console.log(fact);
-}
+```typescript
+has(name: string, ...args: InputTerm): boolean;
 ```
 
-## `has()` and `get()`
+An error will be raised if the number of `args` is not equal to the number of
+arguments that the proposition has.
 
-The `has()` method is intended to check whether a relational proposition
-exists in the database, and the `get()` method is intended to check the value
-of a functional proposition. (But since [these are actually the same
-thing](/docs/language/facts/#everythings-secretly-functional), either can be used
-for either one.) The `has()` method checks for the presence of an attribute (with
-any value), returning a `boolean`. The `get()` method checks for the value
-associated with an attribute, returning the value or `undefined`.
+### `get()` method
+
+The `get()` method is intended to check the value assigned to a functional
+proposition.
 
-Both methods take a string as the first argument, and then one additional
-[`InputTerm`](/docs/api/terms/#inputterm) argument for every non-value
-argument for the predicate.
+```typescript
+get(name: string, ...args: InputTerm): undefined | Term;
+```
+
+An error will be raised if the number of `args` is not equal to the number of
+arguments that the proposition has (not counting the value).
 
 ### Example
 
-In a database with propositions of the form, `node _`, `edge _ _`, and
+Since [functional and relational propositions are actually the same
+thing](/docs/language/facts/#everythings-secretly-functional), either `has()`
+or `get()` can be used with any proposition.
+
+In a solution with propositions of the form `node _`, `edge _ _`, and
 `color _ is _`, the implied Typescript types for `has()` and `get()` are as follows:
 
 ```typescript
@@ -72,7 +72,27 @@ dusa.solution.get('color', 1); // === "blue"
 dusa.solution.get('color', 9); // === undefined
 ```
 
-## `lookup()` method
+## Enumerating all facts
+
+### `facts` getter
+
+The `facts` getter provides an iterator over all the [facts](/docs/api/terms/#type-fact)
+in a solution.
+
+```javascript
+const dusa = new Dusa(`
+    #builtin INT_MINUS minus
+    digit 9.
+    digit (minus N 1) :- digit N, N != 0.`);
+
+for (const fact of dusa.solution.facts) {
+  console.log(fact);
+}
+```
+
+## Querying solutions
+
+### `lookup()` method
 
 The `lookup()` method on solutions is a powerful query mechanism. If your program
 has a relational proposition `path _ _`, then given only the first argument

docs/src/content/docs/docs/api/terms.md

@@ -16,7 +16,7 @@ All Dusa terms have a correspondence with JavaScript types:
 - An uninterpreted function with arguments like `h 9 "fish"` in Dusa corresponds
   to an object `{ name: 'h', args: [9n, 'fish'] }` in JavaScript.
 
-### `Term`
+### type `Term`
 
 ```typescript
 export type Term =
@@ -27,7 +27,7 @@ export type Term =
   | { name: string; args: [Term, ...Term[]] };
 ```
 
-### `Fact`
+### type `Fact`
 
 ```typescript
 export interface Fact {
@@ -43,7 +43,7 @@ The Dusa and DusaSolution methods that take terms and facts as argument accept
 inputs that are more flexible than the outputs that Dusa will return (see the
 [Robustness Principle](https://en.wikipedia.org/wiki/Robustness_principle)).
 
-### `InputTerm`
+### type `InputTerm`
 
 Dusa will accept numbers of type `number` and convert them to
 [BigInt](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/BigInt)
@@ -53,7 +53,7 @@ to Dusa.
 An input constant like `a` can also be given as `{ name: 'a', args: [] }`, even
 though that constant will always be output as `{ name: 'a' }`.
 
-### `InputFact`
+### type `InputFact`
 
 ```typescript
 export interface InputFact {