Update docs, add sudoku as an example.

docs/examples/Sudoku.ejs

@@ -0,0 +1,144 @@
+<%# 等价关系 %>
+
+<%
+for (let i = 1; i <= 9; i++) {
+    for (let j = 1; j <= 9; j++) {
+        if (i === j) {
+%>
+<%- `(${i} = ${j})` %>
+<%
+} else {
+%>
+<%- `(${i} != ${j})` %>
+<%
+}
+}
+}
+%>
+
+<%# 相等与不等 %>
+
+((Cell `x `y) = (Literal `a))
+(`a != `b)
+----------
+((Cell `x `y) != (Literal `b))
+
+<%
+for (let i = 1; i <= 9; i++) {
+    for (let j = 1; j <= 9; j++) {
+        if (i !== j) {
+-%>
+<%- `((Cell \`x \`y) != (Literal ${j}))` %>
+<%
+}
+}
+-%>
+--------------------------------------
+<%- `((Cell \`x \`y) = (Literal ${i}))` %>
+
+<%
+}
+%>
+
+<%# 数独行列 %>
+
+((Cell `x `y) = `n)
+(`x != `x')
+---------------------
+((Cell `x' `y) != `n)
+
+((Cell `x `y) = `n)
+(`y != `y')
+---------------------
+((Cell `x `y') != `n)
+
+<%
+for (let i = 1; i <= 9; i++) {
+    for (let j = 1; j <= 9; j++) {
+        if (i !== j) {
+-%>
+<%- `((Cell \`x ${j}) != \`n)` %>
+<%
+}
+}
+-%>
+-------------------------------------
+<%- `((Cell \`x ${i}) = \`n)` %>
+
+<%
+}
+%>
+
+<%
+for (let i = 1; i <= 9; i++) {
+    for (let j = 1; j <= 9; j++) {
+        if (i !== j) {
+-%>
+<%- `((Cell ${j} \`y) != \`n)` %>
+<%
+}
+}
+-%>
+-------------------------------------
+<%- `((Cell ${i} \`y) = \`n)` %>
+
+<%
+}
+%>
+
+<%# 数独分块 %>
+
+<%
+for (let ib = 1; ib <= 3; ib++) {
+    for (let jb = 1; jb <= 3; jb++) {
+        for (let it = 1; it <= 3; it++) {
+            for (let jt = 1; jt <= 3; jt++) {
+                const xt = (ib - 1) * 3 + it;
+                const yt = (jb - 1) * 3 + jt;
+                for (let i = 1; i <= 3; i++) {
+                    for (let j = 1; j <= 3; j++) {
+                        const x = (ib - 1) * 3 + i;
+                        const y = (jb - 1) * 3 + j;
+                        if (i !== it || j !== jt) {
+%>
+<%- `((Cell ${x} ${y}) = \`n)` %>
+------------------------------------
+<%- `((Cell ${xt} ${yt}) != \`n)` %>
+<%
+}
+}
+}
+}
+}
+}
+}
+%>
+
+<%
+for (let ib = 1; ib <= 3; ib++) {
+    for (let jb = 1; jb <= 3; jb++) {
+        for (let it = 1; it <= 3; it++) {
+            for (let jt = 1; jt <= 3; jt++) {
+                const xt = (ib - 1) * 3 + it;
+                const yt = (jb - 1) * 3 + jt;
+                for (let i = 1; i <= 3; i++) {
+                    for (let j = 1; j <= 3; j++) {
+                        const x = (ib - 1) * 3 + i;
+                        const y = (jb - 1) * 3 + j;
+                        if (i !== it || j !== jt) {
+-%>
+<%- `((Cell ${x} ${y}) != \`n)` %>
+<%
+}
+}
+}
+-%>
+--------------------------------------
+<%- `((Cell ${xt} ${yt}) = \`n)` %>
+
+<%
+}
+}
+}
+}
+%>