1 files changed, 0 insertions, 98 deletions
diff --git a/examples/SUMO/Basic.gf b/examples/SUMO/Basic.gf
deleted file mode 100644
index 19ad57054..000000000
--- a/examples/SUMO/Basic.gf
+++ /dev/null
@@ -1,98 +0,0 @@
---# -path=.:englishExtended:common:prelude:abstract
-abstract Basic = {
-
-cat
-  Class;
-  El Class;
-  Ind Class;
-  SubClass (c1,c2 : Class);
-  Inherits Class Class ;
-  [El Class];
-  [Class];
-  Formula;
-  Desc Class;
-  Var Class;
-  Stmt ;
-
-
--- class-forming operations
-data 
-  both : Class -> Class -> Class ;
-  either : Class -> Class -> Class ;
-  
-  KappaFn : (c : Class) -> (Var c -> Formula) -> Class ;
-
-
--- inheritance between classes   
-data
-  -- simple sub-class relations
-  inhz : (c : Class) -> Inherits c c;
-  inhs : (c1, c2, c3 : Class) -> SubClass c1 c2 -> Inherits c2 c3 -> Inherits c1 c3;
-
-  -- (both c1 c2) is subclass of c1 and of c2
-  bothL : (c1, c2 : Class) -> SubClass (both c1 c2) c1 ;
-  bothR : (c1, c2 : Class) -> SubClass (both c1 c2) c2 ;
-
-  -- relationship with other subclasses
-  bothC : (c1, c2, c3 : Class) -> Inherits c3 c1 -> Inherits c3 c2 -> Inherits c3 (both c1 c2);
-
-  -- (either c1 c2) is superclass of c1 and of c2
-  eitherL : (c1, c2 : Class) -> Inherits c1 (either c1 c2);
-  eitherR : (c1, c2 : Class) -> Inherits c2 (either c1 c2);
-
-  -- relationship with other subclasses
-  eitherC : (c1,c2,c3 : Class) -> SubClass c1 c3 -> SubClass c2 c3 -> SubClass (either c1 c2) c3 ; 
-
-  -- sub-class axiom for KappaFn
-  kappa : (c : Class) -> (p : Var c -> Formula) -> Inherits (KappaFn c p) c ;
-
-
--- coercion from Var to El
-data 
-  var : (c1 , c2 : Class) -> Inherits c1 c2 -> Var c1 -> El c2 ;
-
-
--- coercion from Ind to El 
-data 
-  el : (c1, c2 : Class) -> Inherits c1 c2 -> Ind c1 -> El c2;
-
-
--- first-order logic operations for Formula
-data 
-  not : Formula -> Formula;
-  and : Formula -> Formula -> Formula;
-  or : Formula -> Formula -> Formula;
-  impl : Formula -> Formula -> Formula;
-  equiv : Formula -> Formula -> Formula;
-
--- quantification over instances of a Class
-data
-  exists : (c : Class) -> (Var c -> Formula) -> Formula;
-  forall : (c : Class) -> (Var c -> Formula) -> Formula;
-
-
--- Desc category
-data
-  desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c2 ;
-
-fun descClass : (c : Class) -> Desc c -> Class ;
-def descClass _ (desc c _ _) = c ;
-
-fun descInh : (c : Class) -> (p : Desc c) -> Inherits (descClass c p) c ;
---def descInh c1 (desc c2 c1 i) = i ;
-
-fun desc2desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c1 -> Desc c2 ;
---def desc2desc _ _ inh dsc = desc ? ? (plusInh ? ? ? inh (descInh ? dsc)) ;
-
---fun plusInh : (c1,c2,c3 : Class) -> Inherits c1 c2 -> Inherits c2 c3 -> Inherits c1 c3 ;
---def plusInh _ _ _ inhz                 inh2 = inh2 ;
---    plusInh _ _ _ (inhs _ _ _ sc inh1) inh2 = inhs ? ? ? sc (plusInh ? ? ? inh1 inh2) ;
-
-
--- statements 
-data 
-  subClassStm : (c1,c2 : Class) -> SubClass c1 c2 -> Stmt ;
-  instStm : (c : Class) -> Ind c -> Stmt ;
-  formStm : Formula -> Stmt ;
-
-};