From 80edbd08e13200d2c080ac281d19948bbbcd92e0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 17:09:54 +0200
Subject: Reorganize theory structure. In particular, the identity type moves
 out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

---
 ROOT | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

(limited to 'ROOT')

diff --git a/ROOT b/ROOT
index 09e3042..1e8017c 100644
--- a/ROOT
+++ b/ROOT
@@ -1,15 +1,23 @@
-session Spartan in "spartan/theories" = Pure +
+session Spartan_Core in "spartan/core" = Pure +
   description "
     Spartan type theory: a minimal dependent type theory based on
     intensional Martin-Löf type theory with cumulative Russell-style universes,
-    Pi, Sigma and identity types.
+    Pi, Sigma and identity types. This session consists only of the very core
+    theory files.
   "
   sessions
     "HOL-Eisbach"
   theories
     Spartan (global)
-    Identity
-    Equivalence
+
+session Spartan in spartan = Spartan_Core +
+  description "
+    Type theory based on Spartan, but with a few more bells and whistles.
+  "
+  directories
+    data
+  theories
+    "data/List"
 
 session HoTT in hott = Spartan +
   description "
@@ -21,5 +29,7 @@ session HoTT in hott = Spartan +
   "
   theories
     Base
+    Identity
+    Equivalence
     Nat
 
-- 
cgit v1.2.3