check

Binary.pf

@@ -100,7 +100,7 @@ proof
         = from_binary(node(true,empty))         by definition inc
     ... = suc(2 * 0)                            by definition {from_binary, from_binary}
     ... = 1                                     by rewrite mult_zero[2]
-    ... ={ suc(from_binary(empty)) }            by definition from_binary
+    ... =# suc(from_binary(empty)) #            by definition from_binary
   }
   case node(b, bs') suppose IH: from_binary(inc(bs')) = suc(from_binary(bs')) {
     switch b {
@@ -115,15 +115,15 @@ proof
                   by definition operator+
           ... = suc(suc(from_binary(bs') + from_binary(bs')))
                   by rewrite add_suc[from_binary(bs')][from_binary(bs')]
-          ... ={ suc(suc(2 * from_binary(bs'))) }       by rewrite two_mult[from_binary(bs')]
-          ... ={ suc(from_binary(node(true,bs'))) }     by definition {from_binary}
+          ... =# suc(suc(2 * from_binary(bs'))) #       by rewrite two_mult[from_binary(bs')]
+          ... =# suc(from_binary(node(true,bs'))) #     by definition {from_binary}
       }
       case false {
         equations
               from_binary(inc(node(false,bs')))
             = from_binary(node(true,bs'))               by definition inc
         ... = suc(2 * from_binary(bs'))                 by definition from_binary
-        ... ={ suc(from_binary(node(false,bs'))) }      by definition from_binary
+        ... =# suc(from_binary(node(false,bs'))) #      by definition from_binary
       }
     }
   }

Deduce.lark

@@ -95,7 +95,7 @@ ident: IDENT              -> ident
     | "─"                                          -> omitted_term
     | "(" term ")"                                 -> paren
     | "[" term_list "]"                            -> list_literal
-    | "{" term "}"                                 -> mark
+    | "#" term "#"                                 -> mark
     | "%" type
 
 ?term_list:                                        -> empty

List.pf

@@ -296,7 +296,7 @@ proof
       length(map(node(x,ls'),f))
           = 1 + length(map(ls',f))  by definition {map, length}
       ... = 1 + length(ls')         by rewrite IH
-      ... ={ length(node(x,ls')) }     by definition {length}
+      ... =# length(node(x,ls')) #     by definition {length}
   }
 end
 
@@ -331,8 +331,8 @@ proof
     equations
       map(@empty<T> ++ ys, f)
           = map(ys, f)                  by definition operator++
-      ... ={ @empty<T> ++ map(ys, f) }        by definition operator++
-      ... ={ map(@empty<T>, f) ++ map(ys, f) }  by definition map
+      ... =# @empty<T> ++ map(ys, f) #        by definition operator++
+      ... =# map(@empty<T>, f) ++ map(ys, f) #  by definition map
   }
   case node(x, xs')
     suppose IH: map(xs' ++ ys, f) = map(xs',f) ++ map(ys, f)
@@ -397,7 +397,7 @@ proof
 		by rewrite IH[ys']
         ... = node(pair(f(x), g(y)), map(zip(xs', ys'), λp{pair(f(first(p)), g(second(p)))}))
                by definition pairfun
-	... ={ map(zip(node(x,xs'),node(y,ys')), pairfun(f,g)) }
+	... =# map(zip(node(x,xs'),node(y,ys')), pairfun(f,g)) #
 		by definition {pairfun, first, second}
       }
     }
@@ -817,7 +817,7 @@ proof
     equations
       rev_app(xs', node(x,ys))
           = reverse(xs') ++ node(x,ys) by IH[node(x,ys)]
-      ... = reverse(xs') ++ { (node(x,empty) ++ ys) }
+      ... = reverse(xs') ++ # (node(x,empty) ++ ys) #
             by definition {operator++,operator++}
       ... = (reverse(xs') ++ node(x,empty)) ++ ys
             by symmetric append_assoc<T>[reverse(xs')][node(x,empty),ys]
@@ -861,7 +861,7 @@ proof
   arbitrary xs:List<T>, b:T, f:fn T,T->T
   equations
     foldl(xs, b, f)
-        ={ foldl(xs,foldr(@empty<T>, b, flip(f)), flip(flip(f))) }
+        =# foldl(xs,foldr(@empty<T>, b, flip(f)), flip(flip(f))) #
               by definition foldr and rewrite flip_flip<T>[f]
     ... = foldr(rev_app(xs,empty),b,flip(f))
               by symmetric foldr_rev_app_foldl<T>[xs][empty,b,flip(f)]
@@ -904,7 +904,7 @@ proof
     equations
           head(node(x,xs) ++ R)
         = just(x)                           by definition {operator++,head}
-    ... ={ head(node(x,xs)) }            by definition head
+    ... =# head(node(x,xs)) #            by definition head
   }
 end
 

Makefile

@@ -3,9 +3,14 @@ PYTHON = $(shell command -v python3.11)
 TEST_PASS_DIR = ./test/should-pass
 TEST_ERROR_DIR = ./test/should-error
 
-default: tests check_docs tests-lib
+default: tests tests-lib # check_docs 
 
-check_docs: check_README check_fun check_intro check_ref
+# Problem regarding the docs: github pages markdown is not compatible
+# with using entangled, so the entangled syntax is currently commented
+# out. We need a way to automatically put the entangled syntax back in
+# and then run deduce on these files. -Jeremy
+
+check_docs: check_index check_fun check_intro check_ref
 
 tests-should-pass:
 	$(PYTHON) ./deduce.py --recursive-descent $(TEST_PASS_DIR)
@@ -23,10 +28,10 @@ tests-lib:
 
 tests: tests-should-pass tests-should-error
 
-check_README:
+check_index:
 	/Users/jsiek/Library/Python/3.11/bin/entangled tangle 
-	$(PYTHON) ./deduce.py --recursive-descent README.pf
-	$(PYTHON) ./deduce.py --lalr README.pf
+	$(PYTHON) ./deduce.py --recursive-descent index.pf
+	$(PYTHON) ./deduce.py --lalr index.pf
 
 check_fun:
 	/Users/jsiek/Library/Python/3.11/bin/entangled tangle 
@@ -46,5 +51,5 @@ check_ref:
 	$(PYTHON) ./deduce.py --lalr Reference.pf
 
 clean:
-	rm -f README.pf FunctionalProgramming.pf ProofIntro.pf
+	rm -f index.pf FunctionalProgramming.pf ProofIntro.pf
 	rm -rf .entangled

Nat.pf

@@ -182,7 +182,7 @@ theorem suc_one_add: all n:Nat.
 proof
   arbitrary n:Nat
   equations
-    suc(n) ={ suc(0 + n) }      by definition operator+
+    suc(n) =# suc(0 + n) #      by definition operator+
        ... = suc(0) + n         by symmetric suc_add[0, n]
 end
 
@@ -448,7 +448,7 @@ proof
         by definition {operator*, operator+}
     equations   suc(n + m' * suc(n))
               = suc(n + (m' + m' * n))       by rewrite IH[n]
-          ... = suc( {(n + m') + m' * n} )   by rewrite add_assoc[n][m', m' * n]
+          ... = suc( #(n + m') + m' * n# )   by rewrite add_assoc[n][m', m' * n]
           ... = suc((m' + n) + m' * n)       by rewrite add_commute[n][m']
           ... = suc(m' + (n + m' * n))       by rewrite add_assoc[m'][n, m' * n]
   }
@@ -507,7 +507,7 @@ proof
     equations   0 * (x + y)
               = 0                     by zero_mult[x+y]
           ... = 0 + 0                 by symmetric add_zero[0]
-          ... ={ 0 * x + 0 * y }      by rewrite zero_mult[x] | zero_mult[y]
+          ... =# 0 * x + 0 * y #      by rewrite zero_mult[x] | zero_mult[y]
   }
   case suc(a') suppose IH {
     arbitrary x:Nat, y:Nat
@@ -553,7 +553,7 @@ proof
         = (n + m' * n) * o          by definition operator*
     ... = n * o + (m' * n) * o      by dist_mult_add_right[n, m'*n, o]
     ... = n * o + m' * (n * o)      by rewrite IH[n,o]
-    ... = {suc(m') * (n * o)}   by definition operator*
+    ... =# suc(m') * (n * o) #      by definition operator*
   }
 end
 
@@ -1411,10 +1411,10 @@ proof
   }
   case suc(x') suppose IH {
     equations
-    {max(suc(suc(x')),suc(x'))} = suc(max(suc(x'),x'))
+    # max(suc(suc(x')),suc(x')) #= suc(max(suc(x'),x'))
                                           by definition max
     ... = suc(suc(max(x',x')))            by rewrite IH
-    ... = {suc(max(suc(x'),suc(x')))} by definition max
+    ... =# suc(max(suc(x'),suc(x'))) #    by definition max
   }
 end
 
@@ -2213,7 +2213,7 @@ proof
                        ... = suc(M) * ((n + M * n) + M) + M
                                       by rewrite mult_commute[((n + M * n) + M)][suc(M)]
                        ... = (((n + M * n) + M) + M * ((n + M * n) + M)) + M  by definition operator*
-                       ... = ({n + M * n + M} + M * ((n + M * n) + M)) + M
+                       ... = (#n + M * n + M# + M * ((n + M * n) + M)) + M
                                  by rewrite symmetric add_assoc[n][M*n,M]
                        ... = (n + (M * n + M)) + (M * ((n + M * n) + M) + M)
                                       by rewrite add_assoc[(n + M * n + M)][M * ((n + M * n) + M),M]

Nat.thm

@@ -1,6 +1,6 @@
 This file was automatically generated by Deduce.
 This file summarizes the theorems proved in the file:
-	Nat.pf
+	./Nat.pf
 
 zero_add: (all n:Nat. 0 + n = n)
 

Reference.md

@@ -1047,10 +1047,10 @@ define list_example = node(3, node(8, node(4, empty)))
 ## Mark 
 
 ```
-term ::= "{" term "}"
+term ::= "#" term "#"
 ```
 
-Marking a subterm with curly-braces restricts a `rewrite` or `definition`
+Marking a subterm with hash symbols restricts a `rewrite` or `definition`
 proof to only apply to that subterm.
 
 <!-- {.deduce #mark_example} -->
@@ -1060,9 +1060,9 @@ proof
   arbitrary x:Nat
   suppose: x = 1
   equations
-    {x} + x + x = 1 + x + x   by rewrite recall x = 1
-  $ 1 + {x} + x = 1 + 1 + x   by rewrite recall x = 1
-  $ 1 + 1 + {x} = 1 + 1 + 1   by rewrite recall x = 1
+    #x# + x + x = 1 + x + x   by rewrite recall x = 1
+  $ 1 + #x# + x = 1 + 1 + x   by rewrite recall x = 1
+  $ 1 + 1 + #x# = 1 + 1 + 1   by rewrite recall x = 1
             ... = 3           by definition {operator+,operator+}
 end
 ```
@@ -1121,6 +1121,13 @@ Example:
 assert 2 * 3 = 6
 ```
 
+## MultiSet (Type)
+
+The `MultiSet<T>` type represents the standard mathematical notion of
+a multiset, which is a set that may contain duplicates of an
+element. The `MultiSet<T>` type is defined in `MultiSet.pf`.
+
+
 ## Not
 
 ```
@@ -1286,6 +1293,16 @@ proof ::= reflexive
 The proof `reflexive` proves that `a = a` for any term `a`.
 
 
+## Set (Type)
+
+The `Set<T>` type defined in `Set.pf` represents the standard
+mathematical notion of a set. The empty set is written `∅` and the
+usual set operations such as union `∪`, intersection `∩`, membership
+`∈`, and subset-or-equal `⊆` are all defined in `Set.pf`.  The
+`Set.thm` file provides a summary of the many theorems about sets that
+are proved in `Set.pf`.
+
+
 ## Some (Existential Quantifier)
 
 ```

index.md

@@ -191,7 +191,7 @@ you can use instead.
 <!--  LocalWords:  contra foo sx xy dist mult
  -->
 
-<!-- {.deduce file=README.pf} -->
+<!-- {.deduce file=index.pf} -->
 <!--
 ```
 import List

rec_desc_parser.py

@@ -218,10 +218,10 @@ def parse_term_hi(token_list, i):
     i = i + 1
     return (term, i)
 
-  elif token.type == 'LBRACE':
+  elif token.type == 'HASH':
     i = i + 1
     term, i = parse_term(token_list, i)
-    if token_list[i].type != 'RBRACE':
+    if token_list[i].type != 'HASH':
       error(meta_from_tokens(token_list[i], token_list[i]),
             'expected closing parentheses, not\n\t' \
             + token_list[i].value)

test/should-pass/mark1.pf

@@ -7,8 +7,8 @@ proof
   suppose prem: (Q = P and P)
   have q_p: Q = P
     by prem
-  conclude Q and {Q} by
-  suffices {Q} and P    by rewrite q_p
-  suffices P and P      by rewrite q_p
-  prem
+  conclude Q and #Q# by
+    suffices #Q# and P    by rewrite q_p
+    suffices P and P      by rewrite q_p
+    prem
 end

test/should-pass/mark2.pf

@@ -17,6 +17,6 @@ function g(U) -> bool {
 theorem T: (h(foo) and g(foo)) = (f(foo) and h(foo))
 proof
   // removing the mark causes this to fail, as intended. -Jeremy
-  conclude { h(foo) and g(foo) } = (f(foo) and h(foo))
+  conclude # h(foo) and g(foo) # = (f(foo) and h(foo))
     by definition {h,g}
-end
+end

test/should-pass/mark3.pf

@@ -9,8 +9,8 @@ function f(C) -> bool {
 theorem T: (f(c) and f(c)) = (f(c) and f(c))
 proof
   equations
-     ({f(c)} and f(c)) = (true and f(c))    by definition f
-   $ (true and {f(c)}) = (true and true)    by definition f
-                   ... = ({f(c)} and true)  by definition f
-                   ... = (f(c) and {f(c)})  by definition f
+     (#f(c)# and f(c)) = (true and f(c))    by definition f
+   $ (true and #f(c)#) = (true and true)    by definition f
+                   ... = (#f(c)# and true)  by definition f
+                   ... = (f(c) and #f(c)#)  by definition f
 end