Commit d1a720d7 authored by Andrei Paskevich's avatar Andrei Paskevich

produce a trigger when "eliminate_if" removes a definition

parent 4db16bb5
......@@ -69,9 +69,10 @@ let add_ld axl d = match d with
let vl,e = open_ls_defn ld in
begin match e with
| Term t when has_if t ->
let f = elim_f (ls_defn_axiom ld) in
let nm = ls.ls_name.id_short ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
let hd = t_app ls (List.map t_var vl) t.t_ty in
let f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in
create_prop_decl Paxiom pr f :: axl, (ls, None)
| _ ->
axl, make_ls_defn ls vl (e_map elim_t elim_f e)
......
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