Leonardo de Moura e14c593003 feat: simp +arith for integers (#7011) ... This PR adds `simp +arith` for integers. It uses the new `grind` normalizer for linear integer arithmetic. We still need to implement support for dividing the coefficients by their GCD. It also fixes several bugs in the normalizer.		2025-02-09 21:41:58 +00:00
..
Compiler	fix: don't strip macro scopes in names of specialized LCNF decls (#6930)	2025-02-04 03:43:18 +00:00
Data	feat: parallel progress notifications (#6329)	2025-02-07 16:50:31 +00:00
DocString
Elab	refactor: elaborate forIn notation without extra let (#6977)	2025-02-08 10:32:34 +00:00
Language	feat: parallel progress notifications (#6329)	2025-02-07 16:50:31 +00:00
Linter	chore: linting List (#6970)	2025-02-07 01:44:51 +00:00
Meta	feat: simp +arith for integers (#7011)	2025-02-09 21:41:58 +00:00
Parser	doc: mention Props are equal to True or False (#6998)	2025-02-08 18:11:26 +00:00
ParserCompiler
PrettyPrinter	feat: make all app unexpanders respond to pp.tagAppFns (#6730)	2025-02-02 23:29:12 +00:00
Server	feat: parallel progress notifications (#6329)	2025-02-07 16:50:31 +00:00
Util	feat: frontend & server support for plugins (#6893)	2025-02-04 23:36:18 +00:00
Widget	feat: generalize infoview.maxTraceChildren to the cmdline (#6716)	2025-01-21 02:06:24 +00:00
AddDecl.lean	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
Attributes.lean
AuxRecursor.lean
BuiltinDocAttr.lean
Class.lean
Compiler.lean
CoreM.lean	fix: convert kernel interrupt into elab interrupt (#6988)	2025-02-07 15:55:32 +00:00
Data.lean
Declaration.lean	feat: add support for constructors and axioms to the grind E-matching module (#6839)	2025-01-29 05:22:05 +00:00
DeclarationRange.lean	feat: labeled and unique sorries (#5757)	2024-12-11 23:53:02 +00:00
DocString.lean	feat: recommended_spelling command (#6869)	2025-02-03 11:15:52 +00:00
Elab.lean	feat: #info_trees in command (#6964)	2025-02-06 03:11:53 +00:00
Environment.lean	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
Exception.lean	fix: convert kernel interrupt into elab interrupt (#6988)	2025-02-07 15:55:32 +00:00
Expr.lean	feat: linear integer arith normalizer (#7002)	2025-02-09 04:32:54 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	fix: add a missing case to Level.geq (#2689)	2024-11-19 21:27:00 +00:00
Linter.lean	chore: fix variable names in List lemmas (#6953)	2025-02-05 09:49:14 +00:00
LoadDynlib.lean	feat: Lean.loadPlugin (#6130)	2024-11-27 09:56:31 +00:00
LocalContext.lean	doc: split the docstring of LocalContext (#6340)	2024-12-15 21:35:25 +00:00
Log.lean
Message.lean	feat: generalize infoview.maxTraceChildren to the cmdline (#6716)	2025-01-21 02:06:24 +00:00
Meta.lean	feat: binderNameHint (#6947)	2025-02-06 11:03:27 +00:00
MetavarContext.lean	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00
Modifiers.lean	feat: Environment.addConstAsync (#6691)	2025-01-19 02:00:16 +00:00
MonadEnv.lean
Parser.lean
ParserCompiler.lean	feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)	2025-01-28 23:34:30 +00:00
PrettyPrinter.lean	feat: do not propagate pretty printer errors through messages (#3696)	2024-12-11 04:10:09 +00:00
PrivateName.lean	feat: Environment.addConstAsync (#6691)	2025-01-19 02:00:16 +00:00
ProjFns.lean
ReducibilityAttrs.lean
Replay.lean	refactor: move registration of namespaces on kernel add into elaborator (#6214)	2025-01-18 23:01:29 +00:00
ReservedNameAction.lean
ResolveName.lean	fix: when pretty printing constant names, do not use aliases from "non-API exports" (#5689)	2024-12-10 17:50:50 +00:00
Runtime.lean
ScopedEnvExtension.lean
Server.lean
Structure.lean	feat: Array.insertIdx/eraseIdx take a tactic-provided proof (#6133)	2024-11-20 09:52:38 +00:00
SubExpr.lean
Syntax.lean	feat: inlay hints for auto-implicits (#6768)	2025-02-04 17:36:49 +00:00
ToExpr.lean	feat: upstream ToExpr deriving handler from Mathlib (#6473)	2024-12-31 15:11:53 +00:00
ToLevel.lean	feat: upstream ToLevel from mathlib (#6285)	2024-12-05 05:50:32 +00:00
Util.lean	feat: add Expr.fvarsSubset (#6430)	2024-12-20 22:29:47 +00:00
Widget.lean