Commit 38e8eba5 authored by Sylvain Dailler's avatar Sylvain Dailler

New test for apply

parent ec80a050
module Ex1
use int.Int
function f int : int
predicate p int
axiom B: forall y. let x = f y in x >= 0 -> p y
goal g : p 42
end
module Ex2
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p x y
axiom B: forall y. let x = f y in p x y
goal g : p 17 42
end
module Ex3
type a constant a0: a
type b constant b0: b
type c constant c0: c
function f unit : b
function g unit : c
predicate p a b c
axiom a : forall a.
let b = f () in
let c = g () in
p a b c ->
false
goal g : false
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="5">
<file name="../185_apply.mlw" proved="true">
</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