Leonardo de Moura 6db01d8e48 perf: simpler isDefEq caching ... We don't try to reuse the cache contents between different `isDefEq` calls. Thus, we can cache more results and ignore whether the state of the metavariable context affects them or not. Closes #1102		2022-07-27 19:35:45 -07:00
..
Compiler	chore: cleanup	2022-07-25 22:39:56 -07:00
Data	feat: doc string support for register_simp_attr, register_option, register_builtin_option, declare_config_elab	2022-07-26 18:46:23 -07:00
Elab	fix: add term info at trailing parsers	2022-07-27 18:10:46 -07:00
Linter	feat: allow custom ignore functions for the unused variables linter	2022-07-25 09:16:44 +02:00
Meta	perf: simpler isDefEq caching	2022-07-27 19:35:45 -07:00
Parser	feat: doc strings for declare_syntax_cat	2022-07-27 13:40:08 -07:00
ParserCompiler
PrettyPrinter	refactor: improve FVarId method discoverability	2022-07-25 22:18:58 -07:00
Server	feat: add option pp.showLetValues	2022-07-26 17:53:34 -07:00
Util	chore: cleanup	2022-07-25 22:39:56 -07:00
Widget	feat: add option pp.showLetValues	2022-07-26 17:53:34 -07:00
Attributes.lean	chore: naming convention	2022-07-24 17:44:29 -07:00
AuxRecursor.lean	refactor: use computed fields for Name	2022-07-11 14:19:41 -07:00
Class.lean	feat: store outParam positions	2022-07-11 17:21:31 -07:00
Compiler.lean	feat: add isNoncomputable function for querying whether a given declaration has been marked as "noncomputable" by users	2022-02-16 13:20:31 -08:00
CoreM.lean	refactor: move InfoState to CoreM	2022-07-25 11:57:56 -07:00
Data.lean	feat: add Lean.Rat for implementing decision procedures	2021-09-14 19:18:12 -07:00
Declaration.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
DeclarationRange.lean	chore: use let/if in do blocks	2022-06-13 17:10:14 -07:00
Deprecated.lean	feat: add [deprecated] attribute	2022-07-24 18:06:03 -07:00
DocString.lean	feat: elaborate add_decl_doc	2022-07-27 09:58:49 -07:00
Elab.lean	refactor: add Elab/Calc.lean	2022-07-24 13:30:05 -07:00
Environment.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Eval.lean	chore: unused variables	2022-06-07 17:54:10 -07:00
Exception.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Expr.lean	chore: fix some docstrings	2022-07-27 06:46:00 -07:00
HeadIndex.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Hygiene.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
ImportingFlag.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
InternalExceptionId.lean	chore: cleanup	2022-01-26 09:18:17 -08:00
KeyedDeclsAttribute.lean	chore: doc strings at KeyedDeclsAttribute.lean	2022-07-25 12:20:19 -07:00
LazyInitExtension.lean	chore: remove arbitrary	2022-01-15 12:14:27 -08:00
Level.lean	refactor: add type LevelMVarId (and abbreviation LMarId)	2022-07-24 17:21:45 -07:00
Linter.lean	feat: add unused variables linter	2022-06-03 13:03:52 +02:00
LoadDynlib.lean	feat: replace constant with opaque	2022-06-14 17:02:59 -07:00
LocalContext.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Log.lean	feat: add option warningAsError	2022-07-26 05:57:54 -07:00
Message.lean	refactor: use computed fields for Name	2022-07-11 14:19:41 -07:00
Meta.lean	feat: add evalTerm and Meta.evalExpr	2022-06-28 19:14:40 -07:00
MetavarContext.lean	perf: simpler isDefEq caching	2022-07-27 19:35:45 -07:00
Modifiers.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
MonadEnv.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Parser.lean	fix: bound syntax kind at v:(ppSpace ident) etc.	2022-07-07 11:49:35 +02:00
ParserCompiler.lean	chore: use a[i]! for array accesses that may panic	2022-07-02 15:12:05 -07:00
PrettyPrinter.lean	feat: ppCategory	2022-07-15 10:58:29 +02:00
ProjFns.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
ReducibilityAttrs.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00
ResolveName.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Runtime.lean	feat: replace constant with opaque	2022-06-14 17:02:59 -07:00
ScopedEnvExtension.lean	feat: replace constant with opaque	2022-06-14 17:02:59 -07:00
Server.lean
Structure.lean	chore: cleanup	2022-07-25 22:39:56 -07:00
SubExpr.lean	refactor: use computed fields for Expr	2022-07-11 14:19:41 -07:00
Syntax.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
ToExpr.lean	chore: prepare for Name refactoring	2022-07-11 14:19:41 -07:00
Util.lean	feat: add HasConstCache	2022-03-15 08:39:48 -07:00
Widget.lean	feat: user widgets	2022-07-25 08:01:27 -07:00