Extraction of absurd
Extraction of absurd
is currently assert false
which is perfectly fine. Though, during development it happens that absurd
is temporary used on "todo" branches as one uses assert false
in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
# <line number> <mlw file name>
on the line before assert false