Update to new boxed definition syntax

docs/source/tutorials/Linearity.md

@@ -131,7 +131,7 @@ This is also a very important technique. So, in short, when you need to use a va
 Formality has another primitive for deep-copying values, boxes. When dealing with data, though, you almost never want to use boxes to perform copies, due to the stratification condition, which essentially segregates the language in levels, blocks communication from higher to lower levels. Regardless, they can still be useful sometimes. See, for example, how `map` is defined for lists:
 
 ```javascript
-!map*n : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
+#map*n : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
 | cons => cons(~B, f(list.head), map(list.tail))
 | nil  => nil(~B)
 * nil(~B)

docs/source/tutorials/Recursion.md

@@ -2,7 +2,7 @@
 
 ## Boxed definitions
 
-Since bounded recursive functions are so common, Formality has built-in syntax for them, relying on "boxed definitions". To make a boxed definition, simply annotate it with a `!` instead of a `:`. That has two effects. First, the whole definition is lifted to `level 1`. Second, it allows you to use boxed definitions inside `<>`s: the parser will automatically unbox them for you. For example, instead of this:
+Since bounded recursive functions are so common, Formality has built-in syntax for them, relying on "boxed definitions". To make a boxed definition, prepend `#` to its name. That has two effects. First, the whole definition is lifted to `level 1`. Second, it allows you to use boxed definitions inside `<>`s: the parser will automatically unbox them for you. For example, instead of this:
 
 ```javascript
 foo : !Word
@@ -20,13 +20,13 @@ main : !Word
 We could write:
 
 ```javascript
-!foo : !Word
+#foo : !Word
   40
 
-!bar : !Word
+#bar : !Word
   2
 
-!main : !Word
+#main : !Word
   <foo> + <bar>
 ```
 
@@ -37,14 +37,14 @@ Both programs are the same, except the later is shorter.
 Formality allows you to turn a boxed definition into a recursive function by appending `*N` to its name (where `N` is a new variable, which will track how many times the function was called), and adding a "halt-case" with a `* term` on the last line (where `term` is an expression that will be returned if the function hits its call limit). So, for example, a factorial function could be written as:
 
 ```javascript
-!fact*n : ! {i : Word} -> Word
+#fact*n : ! {i : Word} -> Word
   if i .= 0:
     1
   else:
     i * fact(i - 1)
   * 0
 
-!main : !Word
+#main : !Word
   <fact*100>(12) // 100 is the call limit; write `<fact*>` to use 2^256-1
 ```
 
@@ -59,23 +59,23 @@ Cover things like:
 - Simple recursive functions and boxed definitions
 
     ```javascript
-    !double*N : !{case *n : Nat} -> Nat
+    #double*N : !{case *n : Nat} -> Nat
     | succ => succ(succ(double(n.pred)))
     | zero => zero
 
-    !double.example : !Nat
+    #double.example : !Nat
       <double*>(succ(zero))
     ```
 
 - Polymorphic recursive functions with level-0 parameters
 
     ```javascript
-    !map*N : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
+    #map*N : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
     | cons => cons(~B, f(list.head), map(list.tail))
     | nil  => nil(~B)
     * nil(~B)
 
-    !map.example : !List(Word)
+    #map.example : !List(Word)
       <map*(~Word, ~Word, #{x} x + 1)>(Word$[1,2,3,4])
     ```
 
@@ -90,7 +90,7 @@ Cover things like:
 
 ```javascript
 // ∀ n . n < n+1
-!less_than_succ*N : !{n : Nat, bound : Bound(n, N)} -> Less(n, succ(n))
+#less_than_succ*N : !{n : Nat, bound : Bound(n, N)} -> Less(n, succ(n))
   (case/Bound bound
   | bound_succ => {e}
     let r0 = cong_unstep(~i, ~N, ~e)

docs/source/tutorials/Theorem-Proving.md

@@ -131,7 +131,7 @@ T Bits
 | b1 {pred : Bits}
 | be
 
-!bnot*n : !{*bits : Bits} -> Bits
+#bnot*n : !{*bits : Bits} -> Bits
   (case/Bits bits
   | b0    => {bnot} b1(bnot(pred))
   | b1    => {bnot} b0(bnot(pred))
@@ -142,7 +142,7 @@ T Bits
 Start with the theorem we want to prove:
 
 ```javascript
-!main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
+#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
   ?
   * ?
 ```
@@ -176,7 +176,7 @@ That's because the body of a recursive function is actually the step case of ind
 Let's match against `bits`, using `self` on the motive:
 
 ```javascript
-!main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
+#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
   case/Bits bits
   | b0 => ?
   | b1 => ?
@@ -217,7 +217,7 @@ to   : b0(bnot(n, bnot(n, bs))) ==    bs
 All we need is to add `b0` on both sides. We can do it with `cong`, from the base libraries (`Base@0`):
 
 ```javascript
-!main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
+#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
   case/Bits bits
   | b0 => cong(~Bits, ~Bits, ~(<bnot(n)>)((<bnot(n)>)(pred)), ~pred, ~b0, ~main(pred))
   | b1 => ?
@@ -247,7 +247,7 @@ Type mismatch.
 We can easily complete this proof now:
 
 ```javascript
-!main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
+#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
   case/Bits bits
   | b0 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(pred)), ~pred, ~b0, ~main(pred))
   | b1 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(pred)), ~pred, ~b1, ~main(pred))
@@ -259,7 +259,7 @@ We can easily complete this proof now:
 As usual, it could be simplified with case'd arguments:
 
 ```javascript
-!main*n : !{case bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
+#main*n : !{case bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
 | b0 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(bits.pred)), ~bits.pred, ~b0, ~main(bits.pred))
 | b1 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(bits.pred)), ~bits.pred, ~b1, ~main(bits.pred))
 | be => refl(~be)