Markus Himmel b144107ed5 chore: deprecate Lean.HashMap and Lean.HashSet (#4954) ... This restores all of the imports of `Lean.Data.HashMap` and `Lean.Data.HashSet` so that users actually see the deprecation warnings instead of a "declaration not found" error.		2024-08-08 12:46:10 +00:00
..
CollectAxioms.lean	feat: safer #eval, and #eval! (#4810)	2024-07-23 15:26:56 +00:00
CollectFVars.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CollectLevelParams.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CollectMVars.lean	perf: replace hasMVar by hasExprMVar in CollectMVars, FindMVar (#4451)	2024-06-14 18:06:00 +00:00
Diff.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
FileSetupInfo.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
FindExpr.lean	perf: precise cache for foldConsts (#4871)	2024-07-30 18:35:45 +00:00
FindLevelMVar.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
FindMVar.lean	perf: replace hasMVar by hasExprMVar in CollectMVars, FindMVar (#4451)	2024-06-14 18:06:00 +00:00
FoldConsts.lean	perf: precise cache for foldConsts (#4871)	2024-07-30 18:35:45 +00:00
ForEachExpr.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
ForEachExprWhere.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
HasConstCache.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
Heartbeats.lean	chore: fix Util.Heartbeats module-doc (#3954)	2024-04-22 07:02:58 +00:00
InstantiateLevelParams.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
LakePath.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
LeanOptions.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
MonadBacktrack.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
MonadCache.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
NumApps.lean	feat: theorem diagnostics (#4924)	2024-08-06 01:01:28 +00:00
NumObjs.lean	feat: add Lean.Expr.numObjs (#4754)	2024-07-16 15:52:33 +00:00
OccursCheck.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Path.lean	chore: revert "fix: make import resolution case-sensitive on all platforms" (#4896)	2024-08-01 13:55:37 +00:00
Paths.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
PPExt.lean	fix: set default value of pp.instantiateMVars to true and make the option be effective (#4558)	2024-07-02 22:59:44 +00:00
Profile.lean	doc: profiler	2024-04-03 17:53:36 +02:00
Profiler.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
PtrSet.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
RecDepth.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Recognizers.lean	fix: regression on match expressions with builtin literals (#3521)	2024-02-27 18:49:44 +00:00
ReplaceExpr.lean	perf: Expr.replace (#4799)	2024-07-20 04:53:43 +00:00
ReplaceLevel.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
SafeExponentiation.lean	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00
SCC.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
SearchPath.lean	chore: upstream ToExpr FilePath and compile_time_search_path% (#4453)	2024-07-08 15:41:03 +00:00
ShareCommon.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
Sorry.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
TestExtern.lean	feat: improvements to test_extern command (#3075)	2024-04-24 03:56:16 +00:00
Trace.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00