stdlib: Matrix.get delcared as function

parent e5106b2f
......@@ -14,7 +14,7 @@ module Matrix
predicate valid_index (a: matrix 'a) (r c: int) =
0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (r c: int) : 'a
val function get (a: matrix 'a) (r c: int) : 'a
requires { [@expl:index in matrix bounds] valid_index a r c }
ensures { result = a.elts r c }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment