Compare commits

...

1 Commits

Author SHA1 Message Date
Leonardo de Moura
f6f5971703 fix: missing grind normalization rule 2025-03-29 14:05:34 -07:00
2 changed files with 4 additions and 0 deletions

View File

@@ -106,6 +106,7 @@ init_grind_norm
or_true true_or or_false false_or or_assoc
-- ite
ite_true ite_false ite_true_false ite_false_true
dite_eq_ite
-- Forall
forall_and
-- Exists

View File

@@ -393,3 +393,6 @@ example [Decidable p] : a = true → p → decide p = a := by
example [Decidable p] : false = a ¬p decide p = a := by
grind
example (a : Nat) (p q r : Prop) (h₁ : if _ : a < 1 then p else q) (h₂ : r) : (if a < 1 then p else q) r := by
grind (splits := 0)