]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mml.ml
Initial revision
[helm.git] / helm / interface / mml.ml
diff --git a/helm/interface/mml.ml b/helm/interface/mml.ml
new file mode 100644 (file)
index 0000000..88c2813
--- /dev/null
@@ -0,0 +1,11 @@
+type expr =
+   Null
+ | Mi of string
+ | Mo of string
+ | Mn of string
+ | Mtext of string
+ | Mrow of expr list
+ | Mfenced of string * string * string * expr list (* open, close, separators *)
+type fragment =
+ Math of expr list
+;;