]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
update in bin
[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommTypes.ml
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
new file mode 100644 (file)
index 0000000..f2f8e87
--- /dev/null
@@ -0,0 +1,29 @@
+type text = string
+
+type word = string
+
+type words = word list
+
+type src =
+(* end of line *)
+  | Line  of text 
+(* other text *)
+  | Text  of text 
+(* mark *)
+  | Mark  of text
+(* Key *)
+  | Key   of word * text
+(* title *)
+  | Title of words
+(* section *)
+  | Slice of words
+(* other comment *)
+  | Other of text * text * text
+
+type srcs = src list
+
+type ('s, 't) aproc = 's -> words -> words -> 't
+
+type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
+
+type step = (bool, bool * words * words) astep