Insert identity can be unique just among arrays with the appropriate cell shape

2 files changed, 2 insertions, 2 deletions

diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html
index c8bf6bc0..d4d22610 100644
--- a/docs/spec/inferred.html
+++ b/docs/spec/inferred.html
@@ -10,7 +10,7 @@
 <h2 id="identities">Identities</h2>
 <p>When monadic Fold (<code><span class='Modifier'>´</span></code>) or Insert (<code><span class='Modifier'>˝</span></code>) is called on an array of length 0, BQN attempts to infer a right identity value for the function in order to determine the result. A right identity value for a dyadic function <code><span class='Function'>𝔽</span></code> is a value <code><span class='Value'>r</span></code> such that <code><span class='Value'>e</span><span class='Function'>≡</span><span class='Value'>e</span><span class='Function'>𝔽</span><span class='Value'>r</span></code> for any element <code><span class='Value'>e</span></code> in the domain. For such a value <code><span class='Value'>r</span></code>, the reduction <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> is equivalent to <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for a non-empty list <code><span class='Value'>l</span></code>, because the first application <code><span class='Paren'>(</span><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span><span class='Paren'>)</span> <span class='Function'>𝔽</span> <span class='Value'>r</span></code> gives <code><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span></code>, which is the starting point when no initial value is given. It's thus reasonable to define <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> to be <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for an empty list <code><span class='Value'>l</span></code> as well, giving a result <code><span class='Value'>r</span></code>.</p>
 <p>For Fold, the result of <code><span class='Function'>𝔽</span><span class='Modifier'>´</span></code> on an empty list is defined to be a right identity value for the <em>range</em> of <code><span class='Function'>𝔽</span></code>, if exactly one such value exists. If an identity can't be proven to uniquely exist, then an error results.</p>
-<p>For Insert, <code><span class='Function'>𝔽</span><span class='Modifier'>˝</span></code> on an array of length 0 is defined similarly, but also depends on the cell shape <code><span class='Number'>1</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span></code>. The required domain is the arrays of that shape that also lie in the range of <code><span class='Function'>𝔽</span></code> (over arbitrary arguments, not shape-restricted ones).</p>
+<p>For Insert, <code><span class='Function'>𝔽</span><span class='Modifier'>˝</span></code> on an array of length 0 is defined similarly, but also depends on the cell shape <code><span class='Number'>1</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span></code>. The required domain is the arrays of that shape that also lie in the range of <code><span class='Function'>𝔽</span></code> (over arbitrary arguments, not shape-restricted ones). Furthermore, an identity may be unique among all possible arguments as in the case of Fold, or it may be an array with shape <code><span class='Number'>1</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span></code> and be unique among arrays with that shape. For example, with cell shape <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span></code>, all of <code><span class='Number'>0</span></code>, <code><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code>, and <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code> are identities for <code><span class='Function'>+</span></code>, but <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code> can be used because it is the only indentity with shape <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span></code>, while the other identities aren't unique and can't be used.</p>
 <p>Identity values for the arithmetic primitives below must be recognized. Under Fold, the result is the given identity value, while under Insert, it is the identity value reshaped to the argument's cell shape.</p>
 <table>
 <thead>
diff --git a/spec/inferred.md b/spec/inferred.md
index a12da31b..5b43c0ef 100644
--- a/spec/inferred.md
+++ b/spec/inferred.md
@@ -12,7 +12,7 @@ When monadic Fold (`´`) or Insert (`˝`) is called on an array of length 0, BQN
 
 For Fold, the result of `𝔽´` on an empty list is defined to be a right identity value for the *range* of `𝔽`, if exactly one such value exists. If an identity can't be proven to uniquely exist, then an error results.
 
-For Insert, `𝔽˝` on an array of length 0 is defined similarly, but also depends on the cell shape `1↓≢𝕩`. The required domain is the arrays of that shape that also lie in the range of `𝔽` (over arbitrary arguments, not shape-restricted ones).
+For Insert, `𝔽˝` on an array of length 0 is defined similarly, but also depends on the cell shape `1↓≢𝕩`. The required domain is the arrays of that shape that also lie in the range of `𝔽` (over arbitrary arguments, not shape-restricted ones). Furthermore, an identity may be unique among all possible arguments as in the case of Fold, or it may be an array with shape `1↓≢𝕩` and be unique among arrays with that shape. For example, with cell shape `3‿2`, all of `0`, `2⥊0`, and `3‿2⥊0` are identities for `+`, but `3‿2⥊0` can be used because it is the only indentity with shape `3‿2`, while the other identities aren't unique and can't be used.
 
 Identity values for the arithmetic primitives below must be recognized. Under Fold, the result is the given identity value, while under Insert, it is the identity value reshaped to the argument's cell shape.