Commit 06cb0f6e authored by Sylvain Dailler's avatar Sylvain Dailler

fix #311. Allow "destruct" to destruct "not"

parent 6d112dd4
......@@ -32,6 +32,8 @@ Transformations
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards.
IDE
* display of counterexamples in the Task view has been improved
......
......@@ -321,6 +321,9 @@ let destruct_fmla ~recursive (t: term) =
else
(* The hypothesis is trivial because Cs1 <> Cs2 thus useless *)
[[]]
| Tnot t1 ->
(* Keep toplevel: this is considered an implication *)
destruct_fmla_exception ~toplevel (t_implies t1 t_false)
| Tif (t1, t2, t3) ->
let ts2 =
destruct_fmla_exception ~toplevel:false t2 |>
......
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