Commit 2670d6f9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove tests with empty sessions from the gallery.

parent 143d49dd
module Issue24
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
(* (42:byte) is coerced to (byte'int (42:byte)) *)
goal g : (42:byte) = 2 * 21
(* we should be able to do:
replace 2 (3:byte)
that is (3:byte) should be coerced to (byte'int (3:byte))
*)
goal g2: (3:byte) = 4
(*
goal g1: (if true then 2 else (3:byte)) = 4
*)
end
\ No newline at end of file
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../24_coercions.mlw">
<theory name="Issue24" sum="a27c7cf4122eba5663023be8c3834a97">
<goal name="g">
</goal>
<goal name="g2">
<transf name="cut" arg1="(2 = (3:byte))">
<goal name="g2.0">
</goal>
<goal name="g2.1">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../43_range_module.mlw" proved="true">
<theory name="Issue43" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
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