fix

Readme.md

@@ -2,11 +2,11 @@
 
 Meow lang is a programming language that is designed **not** to be easy to learn and use.
 
-Its main design purpose is to do experiments with "string replacement".
+Its main design purpose is to do experiments with "string substitution".
 
 ## Formal Definition
 
-Currently the definition of replacement of strings are defined by the built-in `replace` function of `String`.
+Currently the definition of substitution of strings are defined by the built-in `replace` function of `String`.
 
 ## Concepts
 
@@ -46,7 +46,7 @@ F
 
 - [Syntax](./docs/Syntax.md)
 - [Encoding](./docs/Encoding.md)
-- [Double Replacement Lemma](./docs/DRL.md)
+- [Double Substitution Lemma](./docs/DSL.md)
 
 ## Examples
 

docs/.gitignore

@@ -0,0 +1 @@
+proof/

docs/DRL.md → docs/DSL.md

@@ -1,4 +1,4 @@
-# Double Replacement Lemma
+# Double Substitution Lemma
 
 $[x/y]([y/x]y)=\begin{cases}
     y, x\subset y\\

docs/Syntax.md

@@ -4,19 +4,6 @@ The layout of the whole program is not stable, but the core expression syntax is
 
 ## Expression
 
-```
-Expression ::=
-            | Expression "+" Term
-            | Term
-
-Term ::=
-      | Literal
-      | MacroApplication
-      | VarName
-      | "{" BlockExpression "}"
-      | "(" Expression ")"
-```
-
 **All expressions can be evaluated to a string literal.**
 
 `literal` is simply a string literal, like `"abc"`, `"lol"`.
@@ -37,13 +24,16 @@ meow2() {
 `meow1` takes no argument, and it simply returns a string literal `"ab"`.
 
 In `meow2`, we see that we have multiple "commands" in the curly bracket.
+
 The syntax is like Rust, the last expression (which has no ";" at the end) in the block is the return value of the block.
 
 `X;Y` means `let X in Y`, so `X;Y;Z` means `let X in (let Y in Z)`.
 
-Different to many languages, `X=Y` requires that both `X` and `Y` are **expressions** (which is basically strings).
+Different to many languages, `X=Y` requires that both `X` and `Y` are **expressions** (which is string).
+
+`X=Y;Z` means that `let X=Y in Z`, which is $[Y/X]Z$ (string substitution).
 
-`X=Y;Z` means that `let X=Y in Z`, which is $[Y/X]Z$ (string replacement).
+`meow2` will return `"bbbbb"`.
 
 The replacement **only** takes place in the `in xxx`. Hence, in `let X in (let Y in Z)`, the replacement of `X` only takes place in `Z` rather than `Y` (but there is a way to let it happen in `Y`, see later explanation).
 

examples/syn.meow

@@ -19,9 +19,9 @@ dr(x,y,z) {
 
 encode(s) {
     var rep = {
-        "\" = "\\";
         "$" = "\$";
         "^" = "\^";
+        "\" = "\\";
         s
     };
     "_^"+ rep +"_$"
@@ -33,9 +33,9 @@ decode(s) {
         "_$" = "";
         s
     };
+    "\\" = "\";
     "\$" = "$";
     "\^" = "^";
-    "\\" = "\";
     rep
 }
 
@@ -54,3 +54,7 @@ if(c,x,y) {
     };
     decode(enc)        
 }
+
+in(x,y) {
+    eq(y,{x=""; y})
+}