ssreflect driver: added matrix.Matrix

ae90b04c · Jean-Christophe Filliâtre · ccb57be4 · ae90b04c
Commit ae90b04c authored Jun 30, 2015 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 10 additions and 0 deletions

drivers/coq-ssreflect.drv drivers/coq-ssreflect.drv +10 -0

No files found.
--- a/drivers/coq-ssreflect.drv
+++ b/drivers/coq-ssreflect.drv
@@ -120,3 +120,13 @@ theory array.Array
  syntax function make "(make %1 %2)"

 end
+
+theory matrix.Matrix
+
+  syntax type matrix "(matrix %1)"
+
+  syntax function get "(matrix_get %1 %2)"
+  syntax function rows "(nrows %1 : int)"
+  syntax function columns "(ncols %1 : int)"
+
+end