Commit 809203f5 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

WIP

parent 50340323
This diff is collapsed.
......@@ -248,7 +248,7 @@ Fixpoint form_substs sub f :=
| Not f => Not (form_substs sub f)
| Op o f f' => Op o (form_substs sub f) (form_substs sub f')
| Quant q v f' =>
let sub := List.filter (fun '(x,_) => negb (x =? v)) sub in
let sub := list_unassoc v sub in
let out_vars := suboutvars sub in
if negb (Vars.mem v out_vars) then
Quant q v (form_substs sub f')
......
......@@ -70,6 +70,9 @@ Fixpoint list_assoc_dft {A B}`{Eqb A} x (l:list (A*B)) (d:B) :=
| (y,z)::l => if x =? y then z else list_assoc_dft x l d
end.
Definition list_unassoc {A B}`{Eqb A} x : list (A*B) -> list (A*B) :=
filter (fun '(y,_) => negb (y =? x)).
Fixpoint list_mem {A}`{Eqb A} x (l:list A) :=
match l with
| [] => false
......
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