Commit 8bbd91c3 authored by Mário Pereira's avatar Mário Pereira

Extraction test: commented [val] declaration that was never used.

Since we are now testing for the inclusion of [val] declarations inside driver,
such a declaration was causing the test to fail. A possibility is to add a
driver to the test.
parent 83189039
......@@ -44,8 +44,10 @@ module TestExtraction
use import int.Int
use import mach.int.Int
val test_val (x: int) : int
ensures { result > x }
(* FIXME: this function is never used.
Use it somewhere and supply a driver? *)
(* val test_val (x: int) : int *)
(* ensures { result > x } *)
let function f_function (y: int) (x: int) : int
requires { x >= 0 }
......
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