VictorTaelin · January 26, 2025 18:02 · Dec 17, 2023 · Dec 17, 2023 · Dec 7, 2023 · Dec 7, 2023
diff --git a/itt-coc.ts b/itt-coc.ts
@@ -5,15 +5,14 @@
 // binders) and a new self encoding based on equality (rather than dependent
 // motives) greatly reduce code size. A more complete file, including
 // superpositions (for optimal unification) is available on the
-// Interaction-Type-Theory repository. Does not handle recursive functions, but
-// will with a minor change (will add tomorrow). Includes type-in-type and no
-// positivity / structural recursion checker. Although it could be made
-// consistent with less code than these would take (and certainly much less code
-// than native inductive datatypes). For example, Elementary Affine Logic could
-// ensure termination with minimal code bloat, if you're happy being restricted
-// to bounded complexity. Nats and other recursive types could then be done via
-// Parigot encodings. Credits also to Franchu and T6 for insights. This is a
-// new development, may have bugs (:
+// Interaction-Type-Theory repository.
+// Credits also to Franchu and T6 for insights.
+
+// NOTE: this is sound but NOT consistent. To make it so, one must supplement
+// it with a termination checker, using any of many available approaches.
+
+// NOTE: this does NOT handle recursive terms. See the comment below for a version
+// that does, using a more conventional bidirectional type checker plus Self.
 
 // Lists
 type List<A> =

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,3 +1,20 @@
+// A nano dependent type-checker featuring inductive types via self encodings.
+// All computation rules are justified by interaction combinator semantics,
+// resulting in major simplifications and improvements over old Kind-Core.
+// Specifically, computable annotations (ANNs) and their counterpart (ANN
+// binders) and a new self encoding based on equality (rather than dependent
+// motives) greatly reduce code size. A more complete file, including
+// superpositions (for optimal unification) is available on the
+// Interaction-Type-Theory repository. Does not handle recursive functions, but
+// will with a minor change (will add tomorrow). Includes type-in-type and no
+// positivity / structural recursion checker. Although it could be made
+// consistent with less code than these would take (and certainly much less code
+// than native inductive datatypes). For example, Elementary Affine Logic could
+// ensure termination with minimal code bloat, if you're happy being restricted
+// to bounded complexity. Nats and other recursive types could then be done via
+// Parigot encodings. Credits also to Franchu and T6 for insights. This is a
+// new development, may have bugs (:
+
 // Lists
 type List<A> =
   | { tag: "Cons"; head: A; tail: List<A> }

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,20 +1,3 @@
-// A nano dependent type-checker featuring inductive types via self encodings.
-// All computation rules are justified by interaction combinator semantics,
-// resulting in major simplifications and improvements over old Kind-Core.
-// Specifically, computable annotations (ANNs) and their counterpart (ANN
-// binders) and a new self encoding based on equality (rather than dependent
-// motives) greatly reduce code size. A more complete file, including
-// superpositions (for optimal unification) is available on the
-// Interaction-Type-Theory repository. Does not handle recursive functions, but
-// will with a minor change (will add tomorrow). Includes type-in-type and no
-// positivity / structural recursion checker. Although it could be made
-// consistent with less code than these would take (and certainly much less code
-// than native inductive datatypes). For example, Elementary Affine Logic could
-// ensure termination with minimal code bloat, if you're happy being restricted
-// to bounded complexity. Nats and other recursive types could then be done via
-// Parigot encodings. Credits also to Franchu and T6 for insights. This is a
-// new development, may have bugs (:
-
 // Lists
 type List<A> =
   | { tag: "Cons"; head: A; tail: List<A> }
@@ -127,7 +110,7 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
   }
 }
 
-// Collapses normalized ANN binders, for type-checking.
+// Type-checking is done by collapsing normalized ANNs.
 function ANN(book: Book, val: Term, typ: Term, dep: number): Term {
   switch (val.tag) {
     // {{x : A} : B}
@@ -193,14 +176,14 @@ function equal(book: Book, a: Term, b: Term, dep: number): boolean {
   return false;
 }
 
-// Due to computable ANNs, type-checking is done by evaluation.
+// With computable ANNs, checking is done by evaluation.
 function check(book: Book) {
   for (var name in book) {
     try {
       show_term(normal(book, Ann(book[name].val, book[name].typ)));
       console.log("\x1b[32m✔ " + name + "\x1b[0m");
     } catch (e) {
-      // FIXME: handle recursive types properly (see Gist comment)
+      // FIXME: handle recursive types properly
       if (e instanceof RangeError) {
         console.log("\x1b[33m? " + name + "\x1b[0m");
       } else {

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -127,7 +127,7 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
   }
 }
 
-
+// Collapses normalized ANN binders, for type-checking.
 function ANN(book: Book, val: Term, typ: Term, dep: number): Term {
   switch (val.tag) {
     // {{x : A} : B}
@@ -193,6 +193,7 @@ function equal(book: Book, a: Term, b: Term, dep: number): boolean {
   return false;
 }
 
+// Due to computable ANNs, type-checking is done by evaluation.
 function check(book: Book) {
   for (var name in book) {
     try {

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -123,7 +123,7 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
     case "App": return App(normal(book, term.fun, dep), normal(book, term.arg, dep));
     case "Slf": return Slf(x => normal(book, term.bod(x), dep+1));
     case "Ann": return ANN(book, normal(book, term.val, dep), normal(book, term.typ, dep), dep);
-    case "Ref": return book[term.nam] ? normal(book, book[term.nam].val, dep) : Ref(term.nam);
+    case "Ref": return Ref(term.nam);
   }
 }
 
@@ -199,8 +199,13 @@ function check(book: Book) {
       show_term(normal(book, Ann(book[name].val, book[name].typ)));
       console.log("\x1b[32m✔ " + name + "\x1b[0m");
     } catch (e) {
-      console.log("\x1b[31m✘ " + name + "\x1b[0m");
-      console.log(e);
+      // FIXME: handle recursive types properly (see Gist comment)
+      if (e instanceof RangeError) {
+        console.log("\x1b[33m? " + name + "\x1b[0m");
+      } else {
+        console.log("\x1b[31m✘ " + name + "\x1b[0m");
+        console.log(e);
+      }
     }
   }
 }
@@ -398,8 +403,8 @@ var code = `
 @Bool : * =
   (Self λself
     ∀(P: *) 
-    ∀(t: ∀(e: (Equal true  self)) P)
-    ∀(f: ∀(e: (Equal false self)) P)
+    ∀(t: ∀(e: (Equal λPλtλf(t (refl *)) self)) P)
+    ∀(f: ∀(e: (Equal λPλtλf(f (refl *)) self)) P)
     P)
 
 @true : Bool =
@@ -423,6 +428,21 @@ var code = `
 @theorem
   : ∀(b: Bool) (Equal (not (not b)) b)
   = λb (bool_match b λb(Equal (not (not b)) b) (refl *) (refl *))
+
+// Natural numbers
+
+@Nat : * =
+  (Self λself
+    ∀(P: *)
+    ∀(s: ∀(n: Nat) ∀(e: (Equal λPλsλz(s n (refl *)) self)) P)
+    ∀(z: ∀(e: (Equal λPλsλz(z (refl *)) self)) P)
+    P)
+
+@zero : Nat =
+  λP λs λz (z (refl *))
+
+@succ : ∀(n: Nat) Nat =
+  λn λP λs λz (s n (refl *))
 `;
 
 check(do_parse_book(code));
diff --git a/itt-coc.ts b/itt-coc.ts
@@ -318,7 +318,7 @@ function parse_term(code: string): [string, (ctx: List<[string, Term]>) => Term]
   if (code[0] === "*") {
     return [code.slice(1), ctx => Set()];
   }
-  // VAl: `$x T`
+  // SLF: `$x T`
   if (code[0] === "$") {
     var [code, nam] = parse_name(code.slice(1));
     //var [code, _  ] = parse_text(code, " ");

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -118,8 +118,8 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
   switch (term.tag) {
     case "Var": return Var(term.val);
     case "Set": return Set();
-    case "Lam": return Lam(x => normal(book, term.bod(x), dep+1));
     case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
+    case "Lam": return Lam(x => normal(book, term.bod(x), dep+1));
     case "App": return App(normal(book, term.fun, dep), normal(book, term.arg, dep));
     case "Slf": return Slf(x => normal(book, term.bod(x), dep+1));
     case "Ann": return ANN(book, normal(book, term.val, dep), normal(book, term.typ, dep), dep);
@@ -193,7 +193,6 @@ function equal(book: Book, a: Term, b: Term, dep: number): boolean {
   return false;
 }
 
-// With computable ANNs, checking is done during normalization
 function check(book: Book) {
   for (var name in book) {
     try {
@@ -213,8 +212,8 @@ function show_term(term: Term, dep: number = 0): string {
   switch (term.tag) {
     case "Var": return num_to_str(term.val);
     case "Set": return "*";
-    case "All": return "∀(" +num_to_str(dep) + ":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
-    case "Lam": return "λ" +num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
+    case "All": return "∀(" + num_to_str(dep) + ":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
+    case "Lam": return "λ" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
     case "App": return "(" + show_term(term.fun, dep) + " " + show_term(term.arg, dep) + ")";
     case "Slf": return "$" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep+1);
     case "Ann": return "{" + show_term(term.val, dep) + ":" + show_term(term.typ, dep) + "}";
@@ -315,9 +314,9 @@ function parse_term(code: string): [string, (ctx: List<[string, Term]>) => Term]
     var [code, _] = parse_text(code, ")");
     return [code, ctx => args.reduce((f, x) => App(f, x(ctx)), fun(ctx))];
   }
-  // ANY: `*`
+  // SET: `*`
   if (code[0] === "*") {
-    return [code.slice(1), ctx => ({ tag: "Slf", bod: x => x })];
+    return [code.slice(1), ctx => Set()];
   }
   // VAl: `$x T`
   if (code[0] === "$") {
@@ -384,7 +383,7 @@ var code = `
 
 // Self Type
 
-@Self : * = λF $self { self: (F self) }
+@Self : ∀(F: Any) * = λF $self { self: (F self) }
 
 // Heterogeneous Equality
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -193,6 +193,7 @@ function equal(book: Book, a: Term, b: Term, dep: number): boolean {
   return false;
 }
 
+// With computable ANNs, checking is done during normalization
 function check(book: Book) {
   for (var name in book) {
     try {

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -383,7 +383,7 @@ var code = `
 
 // Self Type
 
-@Self : Any = λF $self { self: (F self) }
+@Self : * = λF $self { self: (F self) }
 
 // Heterogeneous Equality
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -379,7 +379,7 @@ function do_parse_book(code: string): Book {
 var code = `
 // Any
 
-@Any : $x x = $x x
+@Any : * = $x x
 
 // Self Type
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -387,7 +387,7 @@ var code = `
 
 // Heterogeneous Equality
 
-@Equal : ∀(a: *) ∀(b: *) * =
+@Equal : ∀(a: Any) ∀(b: Any) * =
   λa λb ∀(P: ∀(x: Any) *) ∀(x: (P a)) (P b)
 
 @refl : ∀(a: Any) (Equal a a) =

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -25,15 +25,17 @@ const Nil  = <A>(): List<A>                       => ({ tag: "Nil" });
 // Terms
 type Term =
   | { tag: "Var"; val: number }
+  | { tag: "Set"; }                                   // *
   | { tag: "All"; inp: Term; bod: (x: Term) => Term } // ∀(<x>: <term>) <term>
   | { tag: "Lam"; bod: (x: Term) => Term }            // λx <term>
   | { tag: "App"; fun: Term; arg: Term }              // (<term> <term>)
   | { tag: "Slf"; bod: (x: Term) => Term }            // $<x> <term>
   | { tag: "Ann"; val: Term; typ: Term }              // {<term> : <term>}
   | { tag: "Ref"; nam: string }                       // @term
 const Var = (val: number): Term                       => ({ tag: "Var", val });
-const Lam = (bod: (x: Term) => Term): Term            => ({ tag: "Lam", bod });
+const Set = (): Term                                  => ({ tag: "Set" });
 const All = (inp: Term, bod: (x: Term) => Term): Term => ({ tag: "All", inp, bod });
+const Lam = (bod: (x: Term) => Term): Term            => ({ tag: "Lam", bod });
 const App = (fun: Term, arg: Term): Term              => ({ tag: "App", fun, arg });
 const Slf = (bod: (x: Term) => Term): Term            => ({ tag: "Slf", bod });
 const Ann = (val: Term, typ: Term): Term              => ({ tag: "Ann", val, typ });
@@ -58,8 +60,9 @@ function deref(book: Book, term: Term): Term {
 function reduce(book: Book, term: Term): Term {
   switch (term.tag) {
     case "Var": return Var(term.val);
-    case "Lam": return Lam(term.bod);
+    case "Set": return Set();
     case "All": return All(term.inp, term.bod);
+    case "Lam": return Lam(term.bod);
     case "App": return reduce_app(book, reduce(book, term.fun), term.arg);
     case "Slf": return Slf(term.bod);
     case "Ann": return reduce_ann(book, term.val, reduce(book, term.typ));
@@ -114,6 +117,7 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
   var term = reduce(book, term);
   switch (term.tag) {
     case "Var": return Var(term.val);
+    case "Set": return Set();
     case "Lam": return Lam(x => normal(book, term.bod(x), dep+1));
     case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
     case "App": return App(normal(book, term.fun, dep), normal(book, term.arg, dep));
@@ -156,6 +160,9 @@ function equal(book: Book, a: Term, b: Term, dep: number): boolean {
   if (a.tag === "Var" && b.tag === "Var") {
     return a.val === b.val;
   }
+  if (a.tag === "Set" && b.tag === "Set") {
+    return true;
+  }
   if (a.tag === "Lam" && b.tag === "Lam") {
     return equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep+1);
   }
@@ -204,8 +211,9 @@ function check(book: Book) {
 function show_term(term: Term, dep: number = 0): string {
   switch (term.tag) {
     case "Var": return num_to_str(term.val);
-    case "Lam": return "λ" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
-    case "All": return "∀(" + num_to_str(dep) + ":" + show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
+    case "Set": return "*";
+    case "All": return "∀(" +num_to_str(dep) + ":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
+    case "Lam": return "λ" +num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
     case "App": return "(" + show_term(term.fun, dep) + " " + show_term(term.arg, dep) + ")";
     case "Slf": return "$" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep+1);
     case "Ann": return "{" + show_term(term.val, dep) + ":" + show_term(term.typ, dep) + "}";
@@ -310,7 +318,7 @@ function parse_term(code: string): [string, (ctx: List<[string, Term]>) => Term]
   if (code[0] === "*") {
     return [code.slice(1), ctx => ({ tag: "Slf", bod: x => x })];
   }
-  // SLF: `$x T`
+  // VAl: `$x T`
   if (code[0] === "$") {
     var [code, nam] = parse_name(code.slice(1));
     //var [code, _  ] = parse_text(code, " ");
@@ -369,17 +377,20 @@ function do_parse_book(code: string): Book {
 // -----
 
 var code = `
-// Self Types
+// Any
+
+@Any : $x x = $x x
+
+// Self Type
 
-@Self : * =
-  λF $self { self: (F self) }
+@Self : Any = λF $self { self: (F self) }
 
-// Equality
+// Heterogeneous Equality
 
-@Equal : * =
-  λa λb ∀(P: ∀(x:*) *) ∀(x: (P a)) (P b)
+@Equal : ∀(a: *) ∀(b: *) * =
+  λa λb ∀(P: ∀(x: Any) *) ∀(x: (P a)) (P b)
 
-@refl : ∀(a: *) (Equal a a) =
+@refl : ∀(a: Any) (Equal a a) =
   λa λP λx x
 
 // Boolean
@@ -399,18 +410,19 @@ var code = `
 
 // Boolean Induction
 
-@match : ∀(b: Bool) ∀(P: ∀(x:Bool) *) ∀(t: (P true)) ∀(f: (P false)) (P b) =
+@bool_match : ∀(b: Bool) ∀(P: ∀(x:Bool) *) ∀(t: (P true)) ∀(f: (P false)) (P b) =
   λb λP λt λf (b (P b) λe(e P t) λe(e P f))
 
 // Boolean Negation
 
 @not : ∀(b: Bool) Bool =
-  λb (match b λb(Bool) false true)
+  λb (bool_match b λb(Bool) false true)
 
 // Double Negation Theorem
 
-@theorem : ∀(b: Bool) (Equal (not (not b)) b) =
-  λb (match b λb(Equal (not (not b)) b) (refl *) (refl *))
+@theorem
+  : ∀(b: Bool) (Equal (not (not b)) b)
+  = λb (bool_match b λb(Equal (not (not b)) b) (refl *) (refl *))
 `;
 
 check(do_parse_book(code));
diff --git a/itt-coc.ts b/itt-coc.ts
@@ -15,7 +15,6 @@
 // Parigot encodings. Credits also to Franchu and T6 for insights. This is a
 // new development, may have bugs (:
 
-
 // Lists
 type List<A> =
   | { tag: "Cons"; head: A; tail: List<A> }

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -2,7 +2,7 @@
 // All computation rules are justified by interaction combinator semantics,
 // resulting in major simplifications and improvements over old Kind-Core.
 // Specifically, computable annotations (ANNs) and their counterpart (ANN
-// binders), a new self encoding based on equality (rather than dependent
+// binders) and a new self encoding based on equality (rather than dependent
 // motives) greatly reduce code size. A more complete file, including
 // superpositions (for optimal unification) is available on the
 // Interaction-Type-Theory repository. Does not handle recursive functions, but
@@ -15,6 +15,7 @@
 // Parigot encodings. Credits also to Franchu and T6 for insights. This is a
 // new development, may have bugs (:
 
+
 // Lists
 type List<A> =
   | { tag: "Cons"; head: A; tail: List<A> }

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,19 +1,19 @@
 // A nano dependent type-checker featuring inductive types via self encodings.
 // All computation rules are justified by interaction combinator semantics,
 // resulting in major simplifications and improvements over old Kind-Core.
-// Specifically, computable annotations (ANNs) and a new self encoding based
-// on equality (rather than dependent motives) greatly reduce code size. A
-// more complete file, including superpositions (for optimal unification) is
-// available on the Interaction-Type-Theory repository. Does not handle
-// recursive functions, but will with a minor change (will add tomorrow).
-// Includes type-in-type and no positivity / structural recursion checker.
-// Although it could be made consistent with less code than these would take
-// (and certainly much less code than native inductive datatypes). For example,
-// Elementary Affine Logic could ensure termination with minimal code bloat, if
-// you're happy being restricted to bounded complexity. Nats and other
-// recursive types could then be done via Parigot encodings.
-// Credits also to Franchu and T6 for insights.
-// This is a new development, may have bugs (:
+// Specifically, computable annotations (ANNs) and their counterpart (ANN
+// binders), a new self encoding based on equality (rather than dependent
+// motives) greatly reduce code size. A more complete file, including
+// superpositions (for optimal unification) is available on the
+// Interaction-Type-Theory repository. Does not handle recursive functions, but
+// will with a minor change (will add tomorrow). Includes type-in-type and no
+// positivity / structural recursion checker. Although it could be made
+// consistent with less code than these would take (and certainly much less code
+// than native inductive datatypes). For example, Elementary Affine Logic could
+// ensure termination with minimal code bloat, if you're happy being restricted
+// to bounded complexity. Nats and other recursive types could then be done via
+// Parigot encodings. Credits also to Franchu and T6 for insights. This is a
+// new development, may have bugs (:
 
 // Lists
 type List<A> =

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,6 +1,8 @@
 // A nano dependent type-checker featuring inductive types via self encodings.
 // All computation rules are justified by interaction combinator semantics,
-// resulting in major simplifications and improvements over old Kind-Core. A
+// resulting in major simplifications and improvements over old Kind-Core.
+// Specifically, computable annotations (ANNs) and a new self encoding based
+// on equality (rather than dependent motives) greatly reduce code size. A
 // more complete file, including superpositions (for optimal unification) is
 // available on the Interaction-Type-Theory repository. Does not handle
 // recursive functions, but will with a minor change (will add tomorrow).

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,9 +1,15 @@
 // A nano dependent type-checker featuring inductive types via self encodings.
 // All computation rules are justified by interaction combinator semantics,
-// resulting in major simplifications and improvements over old Kind-Core.
-// A more complete file, including superpositions (for optimal unification)
-// is available on the Interaction-Type-Theory repository. Does not handle
+// resulting in major simplifications and improvements over old Kind-Core. A
+// more complete file, including superpositions (for optimal unification) is
+// available on the Interaction-Type-Theory repository. Does not handle
 // recursive functions, but will with a minor change (will add tomorrow).
+// Includes type-in-type and no positivity / structural recursion checker.
+// Although it could be made consistent with less code than these would take
+// (and certainly much less code than native inductive datatypes). For example,
+// Elementary Affine Logic could ensure termination with minimal code bloat, if
+// you're happy being restricted to bounded complexity. Nats and other
+// recursive types could then be done via Parigot encodings.
 // Credits also to Franchu and T6 for insights.
 // This is a new development, may have bugs (:
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -3,7 +3,7 @@
 // resulting in major simplifications and improvements over old Kind-Core.
 // A more complete file, including superpositions (for optimal unification)
 // is available on the Interaction-Type-Theory repository. Does not handle
-// recursive functions, but should with a minor change (will add tomorrow).
+// recursive functions, but will with a minor change (will add tomorrow).
 // Credits also to Franchu and T6 for insights.
 // This is a new development, may have bugs (:
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -2,7 +2,7 @@
 // All computation rules are justified by interaction combinator semantics,
 // resulting in major simplifications and improvements over old Kind-Core.
 // A more complete file, including superpositions (for optimal unification)
-// is available on the Interaction-Type-Theory repository. Doesnt handle
+// is available on the Interaction-Type-Theory repository. Does not handle
 // recursive functions, but should with a minor change (will add tomorrow).
 // Credits also to Franchu and T6 for insights.
 // This is a new development, may have bugs (:

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -2,7 +2,8 @@
 // All computation rules are justified by interaction combinator semantics,
 // resulting in major simplifications and improvements over old Kind-Core.
 // A more complete file, including superpositions (for optimal unification)
-// is available on the Interaction-Type-Theory repository.
+// is available on the Interaction-Type-Theory repository. Doesnt handle
+// recursive functions, but should with a minor change (will add tomorrow).
 // Credits also to Franchu and T6 for insights.
 // This is a new development, may have bugs (:
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -301,7 +301,7 @@ function parse_term(code: string): [string, (ctx: List<[string, Term]>) => Term]
   if (code[0] === "*") {
     return [code.slice(1), ctx => ({ tag: "Slf", bod: x => x })];
   }
-  // VAl: `$x T`
+  // SLF: `$x T`
   if (code[0] === "$") {
     var [code, nam] = parse_name(code.slice(1));
     //var [code, _  ] = parse_text(code, " ");

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -105,7 +105,6 @@ function normal(book: Book, term: Term, dep: number = 0): Term {
   var term = reduce(book, term);
   switch (term.tag) {
     case "Var": return Var(term.val);
-    case "All": return All(term.inp, x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
     case "Lam": return Lam(x => normal(book, term.bod(x), dep+1));
     case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
     case "App": return App(normal(book, term.fun, dep), normal(book, term.arg, dep));

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -363,7 +363,8 @@ function do_parse_book(code: string): Book {
 var code = `
 // Self Types
 
-@Self : * = λF $self { self: (F self) }
+@Self : * =
+  λF $self { self: (F self) }
 
 // Equality
 

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -400,9 +400,8 @@ var code = `
 
 // Double Negation Theorem
 
-@theorem
-  : ∀(b: Bool) (Equal (not (not b)) b)
-  = λb (match b λb(Equal (not (not b)) b) (refl *) (refl *))
+@theorem : ∀(b: Bool) (Equal (not (not b)) b) =
+  λb (match b λb(Equal (not (not b)) b) (refl *) (refl *))
 `;
 
 check(do_parse_book(code));
diff --git a/itt-coc.ts b/itt-coc.ts
@@ -196,8 +196,8 @@ function check(book: Book) {
 function show_term(term: Term, dep: number = 0): string {
   switch (term.tag) {
     case "Var": return num_to_str(term.val);
-    case "Lam": return "λ"+num_to_str(dep)+" " + show_term(term.bod(Var(dep)), dep + 1);
-    case "All": return "∀("+num_to_str(dep)+":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
+    case "Lam": return "λ" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
+    case "All": return "∀(" + num_to_str(dep) + ":" + show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
     case "App": return "(" + show_term(term.fun, dep) + " " + show_term(term.arg, dep) + ")";
     case "Slf": return "$" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep+1);
     case "Ann": return "{" + show_term(term.val, dep) + ":" + show_term(term.typ, dep) + "}";

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -3,7 +3,7 @@
 // resulting in major simplifications and improvements over old Kind-Core.
 // A more complete file, including superpositions (for optimal unification)
 // is available on the Interaction-Type-Theory repository.
-// Special thanks to Franchu and T6 for insights.
+// Credits also to Franchu and T6 for insights.
 // This is a new development, may have bugs (:
 
 // Lists

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -3,6 +3,7 @@
 // resulting in major simplifications and improvements over old Kind-Core.
 // A more complete file, including superpositions (for optimal unification)
 // is available on the Interaction-Type-Theory repository.
+// Special thanks to Franchu and T6 for insights.
 // This is a new development, may have bugs (:
 
 // Lists

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,6 +1,8 @@
 // A nano dependent type-checker featuring inductive types via self encodings.
 // All computation rules are justified by interaction combinator semantics,
 // resulting in major simplifications and improvements over old Kind-Core.
+// A more complete file, including superpositions (for optimal unification)
+// is available on the Interaction-Type-Theory repository.
 // This is a new development, may have bugs (:
 
 // Lists

diff --git a/itt-coc.ts b/itt-coc.ts
@@ -1,5 +1,6 @@
 // A nano dependent type-checker featuring inductive types via self encodings.
-// All computation rules are justified by interaction combinator semantics.
+// All computation rules are justified by interaction combinator semantics,
+// resulting in major simplifications and improvements over old Kind-Core.
 // This is a new development, may have bugs (:
 
 // Lists