we start a kernel for the version "basic with reverse indexes and global

references"

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 60e0390bddd0156e6ff4802b47d226179b59b10a..4ad04534d4faef4d00ac2ace947c3514f54feaa5 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -8,6 +8,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
 automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi 
 automath/autLexer.cmo: automath/autParser.cmi 
 automath/autLexer.cmx: automath/autParser.cmx 
+basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx 
+basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx 
 toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx 
 toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx 
 toplevel/metaOutput.cmi: toplevel/meta.cmx 

diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 50f1a83b69a100c7c8ca14138cece736e1f93f23..e7aa0ae764bd6c04bbe33ff0cf859fda4658934e 100644 (file)
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -1,6 +1,6 @@
 MAIN = helena
 
-DIRECTORIES = lib automath toplevel
+DIRECTORIES = lib automath basic_rg toplevel
 
 REQUIRES = unix
 

diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make
new file mode 100644 (file)
index 0000000..be84305
--- /dev/null
+++ b/helm/software/lambda-delta/basic_rg/Make
@@ -0,0 +1 @@
+brg

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
new file mode 100644 (file)
index 0000000..a3a32f8
--- /dev/null
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -0,0 +1,15 @@
+module U = NUri
+module A = Aut
+
+type uri = U.uri
+type id = A.id
+
+type binder = Abst | Abbr
+
+type term = Sort of int
+          | LRef of int
+         | GRef of uri
+         | Cast of term * term
+         | Appl of term * term
+         | Bind of id * binder * term * term
+