From c65231b7adc38cb302d4b4bfa0072d894161c5ef Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 3 Nov 2024 11:08:32 -0600 Subject: [PATCH] chore: preprocess options to expose more bv goals --- SSA/Projects/InstCombine/TacticAuto.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 9bcd86f33..e8a6322b7 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -231,10 +231,14 @@ macro "simp_alive_split": tactic => all_goals try intros repeat( all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, - BitVec.Refinement.none_left] + BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] + all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, + BitVec.Refinement.none_left, Option, some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] at * any_goals split all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, - BitVec.Refinement.none_left] + BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] + all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, + BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] at * ) ) )