@@ -193,7 +193,8 @@ More formally, a `mark` is a core with three [arms](/docs/glossary/arm/): `+grab
193`+grow`, and `+grad`. In `+grab` is a series of functions to
193`+grow`, and `+grad`. In `+grab` is a series of functions to
194convert from other `mark`s to the given `mark`. In `+grow` is a
194convert from other `mark`s to the given `mark`. In `+grow` is a
195series of functions to convert from the given `mark` to other
195series of functions to convert from the given `mark` to other
196−`mark`s. In `+grad` is `+diff`, `+pact`, `+join`, and `+mash`.
196+`mark`s. In `+grad` is `+diff`, `+pact`, `+join`, and `+mash`, and
198The types are as follows, in an informal pseudocode:
199The types are as follows, in an informal pseudocode:
@@ -207,6 +208,7 @@ The types are as follows, in an informal pseudocode:
207 ++ txt: <mark-type> -> <txt>
208 ++ txt: <mark-type> -> <txt>
211+ ++ form: <mark-type>
210 ++ diff: (<mark-type>, <mark-type>) -> <diff-type>
212 ++ diff: (<mark-type>, <mark-type>) -> <diff-type>
211 ++ pact: (<mark-type>, <diff-type>) -> <mark-type>
213 ++ pact: (<mark-type>, <diff-type>) -> <mark-type>
212 ++ join: (<diff-type>, <diff-type>) -> <diff-type> or NULL
214 ++ join: (<diff-type>, <diff-type>) -> <diff-type> or NULL
@@ -220,12 +222,11 @@ in the general case.
220In general, for a particular `mark`, the `+grab` and `+grow` entries
222In general, for a particular `mark`, the `+grab` and `+grow` entries
221(if they exist) should be inverses of each other.
223(if they exist) should be inverses of each other.
223−In `+grad`, `+diff` takes two instances of a `mark` and produces
225+In `+grad`, `+diff` takes two instances of a `mark` and produces a diff of them
224−a diff of them. `+pact` takes an instance of a `mark` and patches
226+whose `mark` is given by `+form`. `+pact` takes an instance of a `mark` and
225−it with the given diff. `+join` takes two diffs and attempts to
227+patches it with the given diff. `+join` takes two diffs and attempts to merge
226−merge them into a single diff. If there are conflicts, it
228+them into a single diff. If there are conflicts, it produces null. `+mash` takes
227−produces null. `+mash` takes two diffs and forces a merge,
228−annotating any conflicts.
229+two diffs and forces a merge, annotating any conflicts.
230In general, if `+diff` called with A and B produces diff D, then
231In general, if `+diff` called with A and B produces diff D, then
231`+pact` called with A and D should produce B. Also, if `+join`
232`+pact` called with A and D should produce B. Also, if `+join`