Skip to content

Commit 5115dd0

Browse files
authored
Merge pull request #47 from dgpv/patch-4
Fix mistypes: nsat -> dsat
2 parents 027b422 + 6b95a7f commit 5115dd0

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

index.html

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -485,7 +485,7 @@ <h4>Basic satisfactions</h4>
485485
<tr><td><code>c:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
486486
<tr><td><code>d:<em>X</em></code></td><td>0</td><td>sat(<em>X</em>) 1</td></tr>
487487
<tr><td><code>v:<em>X</em></code></td><td>-</td><td>sat(<em>X</em>)</td></tr>
488-
<tr><td><code>j:<em>X</em></code></td><td>0; <span class="text-muted">[nsat(<em>X</em>) (if nonzero top stack)]</span></td><td>sat(<em>X</em>)</td></tr>
488+
<tr><td><code>j:<em>X</em></code></td><td>0; <span class="text-muted">[dsat(<em>X</em>) (if nonzero top stack)]</span></td><td>sat(<em>X</em>)</td></tr>
489489
<tr><td><code>n:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
490490
</tbody>
491491
</table>
@@ -500,7 +500,7 @@ <h4>Basic satisfactions</h4>
500500

501501
<p>
502502
A conservative simplification is made here, ignoring the existence of always-true expressions like <code>1</code>. This makes the typing rules incorrect in the following cases:<ul>
503-
<li><code>or_b(<em>X</em>,1)</code> and <code>or_b(1,<em>X</em>)</code> are complete when <em>X</em> is dissatisfiable ("d"). In that case, the condition is equivalent to 1 and is always met, and a satisfaction of the form "nsat(<em>X</em>)" exists.
503+
<li><code>or_b(<em>X</em>,1)</code> and <code>or_b(1,<em>X</em>)</code> are complete when <em>X</em> is dissatisfiable ("d"). In that case, the condition is equivalent to 1 and is always met, and a satisfaction of the form "dsat(<em>X</em>)" exists.
504504
<li><code>or_b(1,1)</code> is complete, as it is equivalent to 1 and "" is a valid satisfaction.</li>
505505
<li><code>and_b(<em>X</em>,1)</code> and <code>and_b(1,<em>X</em>)</code> are dissatisfiable ("d") when <em>X</em> is.
506506
<li><code>andor(1,1,<em>Z</em>)</code> is complete, as it is equivalent to 1 and "" is a valid satisfaction.</li>

0 commit comments

Comments
 (0)