Commit 35ffacad authored by Sylvain Dailler's avatar Sylvain Dailler

[transform apply] let is now a premise for applied condition of apply

parent 442bffc9
module Test
function f int : int = 17
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
<?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_let.mlw" proved="true">
<theory name="Test" proved="true">
<goal name="g" proved="true">
<transf name="apply" proved="true" arg1="B">
<goal name="g.0" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -35,6 +35,10 @@ let intros f =
| Tquant (Tforall, fq) ->
let vsl, _, fs = t_open_quant fq in
intros_aux lp (lv @ vsl) fs
| Tlet (t, tb) ->
let vs, t2 = t_open_bound tb in
let f = t_equ (t_var vs) t in
intros_aux (f :: lp) ([vs] @ lv) t2
| _ -> (lp, lv, f) in
intros_aux [] [] f
......
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