Commit 06660d8b authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

"triggers, go home", cont.

parent a98734ca
......@@ -77,7 +77,7 @@ let add_ld axl d = match d with
let nm = ls.ls_name.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
let hd = t_app ls ( t_var vl) t.t_ty in
let f = f_forall_close vl [[Term hd]] (elim_f (f_equ hd t)) in
let f = f_forall_close vl [] (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)
......@@ -46,7 +46,7 @@ let inv acc (ps,al) =
let hd = f_app ps tl in
let dj = Util.map_join_left (exi tl) f_or al in
let hsdj = Simplify_formula.fmla_remove_quant (f_implies hd dj) in
let ax = f_forall_close vl [[Fmla hd]] hsdj in
let ax = f_forall_close vl [] hsdj in
let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
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