Leonardo de Moura 5a6f45a324 feat: improve cutsat Nat support (#7876) ... This PR eliminates another source of facts of the form `-1 * NatCast.natCast x <= 0` for each `x : Nat` in the local context. These facts are now stored internally in the cutsat state. cc @kim-em		2025-04-08 19:40:45 +00:00
..
AC	chore: use ∅ notation in favour of .empty functions (#7446)	2025-03-12 04:22:40 +00:00
Grind	feat: improve cutsat Nat support (#7876)	2025-04-08 19:40:45 +00:00
Simp	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
Try	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
AC.lean
Acyclic.lean
Apply.lean
Assert.lean
Assumption.lean
AuxLemma.lean	refactor: use mkAuxLemma in mkAuxTheorem (#7762)	2025-03-31 22:50:30 +00:00
Backtrack.lean
Cases.lean
Cleanup.lean
Clear.lean
Congr.lean
Constructor.lean
Contradiction.lean
Delta.lean
ElimInfo.lean
ExposeNames.lean
Ext.lean
FunInd.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
FunIndCollect.lean
FunIndInfo.lean
FVarSubst.lean
Generalize.lean
Grind.lean	fix: grind ematch theorem activation issue (#7861)	2025-04-07 21:09:26 +00:00
IndependentOf.lean
Induction.lean
Injection.lean
Intro.lean
LibrarySearch.lean
NormCast.lean
Refl.lean
Rename.lean
Repeat.lean
Replace.lean
Revert.lean
Rewrite.lean
Rewrites.lean	feat: validate, expose names, and add hovers for all suggestion tactics (#7474)	2025-04-07 01:11:39 +00:00
Rfl.lean
Simp.lean
SolveByElim.lean
Split.lean	chore: revert "feat: make isRfl lazy"	2025-03-27 11:55:14 +01:00
SplitIf.lean
Subst.lean
Symm.lean
Try.lean
TryThis.lean	feat: make TryThis work in widget messages (#7610)	2025-04-08 16:01:03 +00:00
Unfold.lean	chore: revert "feat: make isRfl lazy"	2025-03-27 11:55:14 +01:00
UnifyEq.lean
Util.lean