Henrik Böving ecba8529cc doc: Leo-Henrik retreat doc (#3869) ... Part of the retreat Hackathon. --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Mario Carneiro <di.gama@gmail.com>		2024-04-12 09:14:31 +00:00
..
ArgsPacker	refactor: ArgsPacker (#3621)	2024-03-14 14:59:40 +00:00
Match	fix: do not lift (<- ...) over pure if-then-else (#3820)	2024-04-01 21:33:59 +00:00
Tactic	fix: offset typeclass checking in simp rules (#3838)	2024-04-07 13:43:59 +00:00
AbstractMVars.lean	fix: do not lift (<- ...) over pure if-then-else (#3820)	2024-04-01 21:33:59 +00:00
AbstractNestedProofs.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
ACLt.lean	fix: loose bound variables at ACLt (#3819)	2024-04-01 20:26:20 +00:00
AppBuilder.lean	refactor: ArgsPacker (#3621)	2024-03-14 14:59:40 +00:00
ArgsPacker.lean	chore: remove the coercion from String to Name (#3589)	2024-03-21 23:46:03 +00:00
Basic.lean	doc: Leo-Henrik retreat doc (#3869)	2024-04-12 09:14:31 +00:00
Canonicalizer.lean	refactor: Canonicalizer: run getFunInfo on expression, not key (#3875)	2024-04-10 20:41:15 +00:00
Check.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CheckTactic.lean	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508)	2024-03-04 23:56:30 +00:00
Closure.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Coe.lean	refactor: Offset.lean and related files (#3614)	2024-03-05 19:40:15 -08:00
CoeAttr.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CollectFVars.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CollectMVars.lean	chore: upstream solve_by_elim (#3408)	2024-02-21 01:16:04 +00:00
CompletionName.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
CongrTheorems.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Constructions.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
CtorRecognizer.lean	feat: better support for reducing Nat.rec (#3616)	2024-03-06 13:28:07 +00:00
DecLevel.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
DiscrTree.lean	doc: for issue #2835	2024-03-06 15:29:04 -08:00
DiscrTreeTypes.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Eqns.lean	fix: matcher splitter is code (#3815)	2024-04-01 02:14:14 +00:00
Eval.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
ExprDefEq.lean	fix: .yesWithDeltaI behavior (#3816)	2024-04-01 02:36:35 +00:00
ExprLens.lean	doc: fix typos (#3543)	2024-02-29 13:23:19 +00:00
ExprTraverse.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
ForEachExpr.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
FunInfo.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
GeneralizeTelescope.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
GeneralizeVars.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
GetUnfoldableConst.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
GlobalInstances.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
IndPredBelow.lean	chore: remove the coercion from String to Name (#3589)	2024-03-21 23:46:03 +00:00
Inductive.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
InferType.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Injective.lean	fix: bug at elimOptParam (#3595)	2024-03-04 23:56:00 +00:00
Instances.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Iterator.lean	chore: address copyright inconsistencies (#3448)	2024-02-22 06:23:50 -08:00
KAbstract.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
KExprMap.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
LazyDiscrTree.lean	feat: weight lazy discriminator tree results early matches (#3818)	2024-04-02 07:19:30 +00:00
LevelDefEq.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
LitValues.lean	chore: use let_expr to cleanup code	2024-03-02 10:07:15 -08:00
Match.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
MatchUtil.lean	fix: regression on match expressions with builtin literals (#3521)	2024-02-27 18:49:44 +00:00
NatInstTesters.lean	refactor: Offset.lean and related files (#3614)	2024-03-05 19:40:15 -08:00
Offset.lean	fix: offset typeclass checking in simp rules (#3838)	2024-04-07 13:43:59 +00:00
PPGoal.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
RecursorInfo.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Reduce.lean	fix: fold raw Nat literals at dsimp (#3624)	2024-03-06 18:29:20 +00:00
ReduceEval.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
SizeOf.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Structure.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
SynthInstance.lean	fix: eta-expanded instances at SynthInstance.lean (#3638)	2024-03-08 20:37:38 +00:00
Tactic.lean	feat: upstream rw? tactic (#3719)	2024-03-23 05:01:35 +00:00
Transform.lean	chore: use builtin_dsimproc when appropriate	2024-03-05 14:42:05 -08:00
TransparencyMode.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
UnificationHint.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
WHNF.lean	fix: .yesWithDeltaI behavior (#3816)	2024-04-01 02:36:35 +00:00