Leonardo de Moura f312170f21 feat: cooper resolution in cutsat (#7339) ... This PR implements cooper conflict resolution in the cutsat procedure. It also fixes several bugs in the proof term construction. We still need to add more tests, but we can already solve the following example that `omega` fails to solve: ```lean example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -10 ≤ 7*x - 9*y → 7*x - 9*y ≤ 4 → False := by grind ```		2025-03-05 03:37:45 +00:00
..
Control	chore: post-#7100 cleanup (#7196)	2025-02-23 22:46:22 +00:00
Data	feat: cooper resolution in cutsat (#7339)	2025-03-05 03:37:45 +00:00
Grind	feat: proof generation for cooper_dvd_left and variants in cutsat (#7312)	2025-03-04 00:40:31 +00:00
Internal	chore: update code after #7110	2025-02-17 18:21:10 +01:00
Omega	chore: aligning Int.ediv/fdiv/tdiv theorems (#7266)	2025-02-28 05:27:40 +00:00
System	feat: Environment.realizeConst (#7076)	2025-02-26 19:32:21 +00:00
BinderNameHint.lean	feat: binderNameHint in congr (#7053)	2025-02-13 09:38:42 +00:00
BinderPredicates.lean
ByCases.lean	feat: nested well-founded recursion via automatic preprocessing (#6744)	2025-02-10 16:43:41 +00:00
Classical.lean	doc: fix typo (#7067)	2025-02-13 13:21:18 +00:00
Coe.lean
Control.lean
Conv.lean	feat: add simp? and dsimp? in conversion mode (#6593)	2025-01-10 01:42:17 +00:00
Core.lean	chore: post-#7100 cleanup (#7196)	2025-02-23 22:46:22 +00:00
Data.lean	feat: add support for Float32 to the Lean runtime (#6348)	2024-12-09 21:33:43 +00:00
Dynamic.lean
Ext.lean
GetElem.lean	chore: use as[i] instead of as.get i	2025-02-19 08:48:33 +11:00
Grind.lean	feat: improve grind failure message (#6633)	2025-01-14 01:10:47 +00:00
Guard.lean
Hints.lean
Internal.lean	feat: partial_fixpoint: theory (#6477)	2025-01-02 09:39:18 +00:00
MacroTrace.lean
Meta.lean	feat: cleanup of get and back functions on List/Array (#7059)	2025-02-17 01:43:45 +00:00
MetaTypes.lean	feat: zetaUnused option (option only) (#6754)	2025-01-23 14:37:41 +00:00
Notation.lean	feat: premise selection API (#7061)	2025-02-14 04:08:18 +00:00
NotationExtra.lean	chore: post-#7100 cleanup (#7196)	2025-02-23 22:46:22 +00:00
Omega.lean	chore: update copyrights (#5449)	2024-09-24 05:27:53 +00:00
Prelude.lean	feat: allow cond to be used in proofs (#7141)	2025-03-04 12:10:29 +00:00
PropLemmas.lean	feat: add BitVec.[(getMsbD, msb)_extractLsb', (getLsbD, getMsbD, msb)_extractLsb] , add and_eq_decide, or_eq_decide, decide_eq_true_iff to bool_to_prop (#6792)	2025-02-17 03:02:37 +00:00
RCases.lean	feat: add generalization hypotheses to induction tactic (#7103)	2025-02-18 03:46:23 +00:00
ShareCommon.lean	feat: USize.size inequalities (#6203)	2024-11-26 23:42:15 +00:00
SimpLemmas.lean	chore: run Batteries linter on Lean (#6364)	2024-12-13 01:28:53 +00:00
Simproc.lean
SizeOf.lean	refactor: name the default SizeOf instance (#5981)	2024-11-07 09:21:32 +00:00
SizeOfLemmas.lean	chore: simp_arith has been deprecated (#7043)	2025-02-12 03:55:45 +00:00
Syntax.lean	feat: rename Array.setD to setIfInBounds (#6195)	2024-11-24 08:54:19 +00:00
System.lean
Tactics.lean	feat: fun_induction foo (no arguments) (#7101)	2025-02-18 12:27:21 +00:00
TacticsExtra.lean	feat: activate new tactic configuration syntax for most tactics (#5898)	2024-11-01 02:08:53 +00:00
Try.lean	feat: compress try? suggestions (#6994)	2025-02-07 19:17:25 +00:00
Util.lean	feat: generalize panic to Sort (#6333)	2024-12-15 21:36:45 +00:00
WF.lean	feat: nested well-founded recursion via automatic preprocessing (#6744)	2025-02-10 16:43:41 +00:00
WFTactics.lean	feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932)	2024-11-03 16:23:37 +00:00
While.lean	chore: make 'while' available earlier (#5784)	2024-10-21 05:56:37 +00:00