- we updated some preambles to match that of nUri.ml

[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index a3a32f8d0fd6855a3b0d21295488e9847364d4c9..09d2f247a33f8078193cee8b688f2a1489df1b69 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -1,15 +1,26 @@
-module U = NUri
-module A = Aut
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
 
-type uri = U.uri
-type id = A.id
+type uri = NUri.uri
+type id = Aut.id
 
-type binder = Abst | Abbr
+type bind = Abst | Abbr (* abstraction, abbreviation *)
 
-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
-         
+type term = Sort of int                     (* hierarchy index *)
+          | LRef of int                     (* reverse de Bruijn index *)
+         | GRef of uri                     (* reference *)
+         | Cast of term * term             (* type, term *)
+         | Appl of term * term             (* argument, function *)
+         | Bind of id * bind * term * term (* name, binder, content, scope *)
+
+type entry = uri * bind * term (* uri, binder, contents *)
+
+type item = entry option