Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-28 18:23 19a9bdc2

View on Github →

fix(tactic/omega): reify nonconstant ints and nats (#1748)

Estimated changes

modified def omega.int.dnf
modified def omega.int.dnf_core
modified theorem omega.int.implies_neg_elim
modified def omega.int.is_nnf
modified theorem omega.int.is_nnf_nnf
modified theorem omega.int.is_nnf_push_neg
modified def omega.int.neg_elim
modified def omega.int.neg_free
modified theorem omega.int.neg_free_neg_elim
modified def omega.int.nnf
modified theorem omega.int.nnf_equiv
modified def omega.int.push_neg
deleted def omega.int.form.repr
deleted def omega.int.form.sat
deleted theorem omega.int.form.sat_or
deleted inductive omega.int.form
added inductive omega.int.preform
modified def omega.int.univ_close
modified def omega.nat.dnf
modified def omega.nat.dnf_core
modified theorem omega.nat.exists_clause_sat
deleted def omega.nat.form.repr
deleted def omega.nat.form.sat
deleted theorem omega.nat.form.sat_or
deleted inductive omega.nat.form
added inductive omega.nat.preform
modified def omega.nat.univ_close
modified theorem omega.nat.implies_neg_elim
modified def omega.nat.is_nnf
modified theorem omega.nat.is_nnf_nnf
modified theorem omega.nat.is_nnf_push_neg
modified def omega.nat.neg_elim
modified theorem omega.nat.neg_free_neg_elim
modified def omega.nat.nnf
modified theorem omega.nat.nnf_equiv
modified def omega.nat.push_neg
modified def omega.nat.is_diff
modified theorem omega.nat.sat_sub_elim
modified def omega.nat.sub_elim