wip

Deducteam · Jan 28, 2025 · 7392193 · 7392193
1 parent ead8c85
commit 7392193
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml
@@ -205,12 +205,12 @@ let rec translate_prop : config -> l2y -> term -> l2y * Why3.Term.term =
   let default m t =
     try
       let sym = List.assoc_eq (Eval.eq_modulo []) t m.t2ls in
-      (m, Why3.Term.ps_app sym [])
+      m, Why3.Term.ps_app sym []
     with Not_found ->
       let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "X") [] in
       if Logger.log_enabled() then
         log "abstract [%a] as psymbol %a" term t Why3.Pretty.print_ls sym;
-      ({m with t2ls = (t,sym)::m.t2ls}, Why3.Term.ps_app sym [])
+      {m with t2ls = (t,sym)::m.t2ls}, Why3.Term.ps_app sym []
   in
   fun cfg m t ->
   if Logger.log_enabled() then log "translate_prop %a [%a]" l2y m term t;

diff --git a/tests/OK/why3.lp b/tests/OK/why3.lp
@@ -27,9 +27,13 @@ opaque symbol test9 a p : π (¬ (`∃ x:τ a, p x) ⇔ (`∀ x, ¬ (p x))) ≔
 
 opaque symbol test10 a p x q : π ((`∀ x:τ a, p x ⇒ q) ⇒ p x ⇒ q) ≔ begin why3 end;
 
+//opaque symbol test a p x q : π ((`∀ x:τ a, p x ⇒ (λ y, q y) x) ⇒ p x ⇒ (λ y, q y) x) ≔ begin why3 end;
+
+//opaque symbol test a p x q : π ((`∀ x:τ a, p x ⇒ q ((λ y,y)x)) ⇒ p x ⇒ q ((λ y,y)x)) ≔ begin why3 end;
+
 //constant symbol o:Set;
 //rule τ o ↪ Prop;
 
-//opaque symbol test10 a (p:τ(nat ⤳ o)) : π (¬ (`∃ x:τ a, p x) ⇔ (`∀ x, ¬ (p x))) ≔ begin why3 end;
+//opaque symbol test a (p:τ(nat ⤳ o)) : π (¬ (`∃ x:τ a, p x) ⇔ (`∀ x, ¬ (p x))) ≔ begin why3 end;
 
-//opaque symbol test10 : π (`∃ p, p ⇒ p) ≔ begin why3 end;
+//opaque symbol test : π (`∃ p, p ⇒ p) ≔ begin why3 end;