max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Kyle Miller 48a9bfb73d
doc: add docstrings to mkFreshUserName etc (#7947) 
This PR adds some docstrings to clarify the functions of
`Lean.mkFreshId`, `Lean.Core.mkFreshUserName`,
`Lean.Elab.Term.mkFreshBinderName`, and
`Lean.Meta.mkFreshBinderNameForTactic`.
2025-04-14 04:17:45 +00:00
..
ArgsPacker chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Constructions feat: align lemmas about List.getLast(!?) with Array/Vector.back(!?) (#7205) 2025-02-24 11:48:43 +00:00
Match chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00
Tactic doc: add docstrings to mkFreshUserName etc (#7947) 2025-04-14 04:17:45 +00:00
AbstractMVars.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
AbstractNestedProofs.lean refactor: use mkAuxLemma in mkAuxTheorem (#7762) 2025-03-31 22:50:30 +00:00
ACLt.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
AppBuilder.lean perf: Environment blocker removals from async-proofs branch (#7483) 2025-03-14 13:37:01 +00:00
ArgsPacker.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
Basic.lean fix: cancellation of synchronous part of previous elaboration (#7882) 2025-04-10 11:43:41 +00:00
BinderNameHint.lean chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00
Canonicalizer.lean chore: remove the old Lean.Data.HashMap implementation (#7519) 2025-03-20 23:49:55 +00:00
Check.lean chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00: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 refactor: use mkAuxLemma in mkAuxTheorem (#7762) 2025-03-31 22:50:30 +00:00
Coe.lean doc: docstring review for monads and transformers (#7548) 2025-03-20 12:18:46 +00:00
CoeAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CollectFVars.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
CollectMVars.lean chore: cleanup after export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
CompletionName.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
CongrTheorems.lean fix: transparency setting when computing congruence lemmas in grind (#7760) 2025-03-31 20:52:36 +00:00
Constructions.lean refactor: Split Constructions module (#4656) 2024-07-05 08:25:44 +00:00
CtorRecognizer.lean fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offsets (#6270) 2024-12-01 18:04:32 +00:00
DecLevel.lean chore: missing registerTraceClass (#4369) 2024-06-06 00:53:16 +00:00
Diagnostics.lean fix: add workaround for MessageData limitations (#6669) 2025-01-16 16:58:20 +00:00
DiscrTree.lean feat: allow line-wrapping when printing DiscrTree.Keys (#7200) 2025-02-24 07:52:47 +00:00
DiscrTreeTypes.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Eqns.lean perf: remove more async blockers (#7497) 2025-03-15 11:07:04 +00:00
Eval.lean perf: async optimizations for Init.Data.BitVec.Lemmas (#7546) 2025-03-18 12:56:16 +00:00
ExprDefEq.lean feat: zetaUnused option (implementation) (#6755) 2025-01-26 11:14:12 +00:00
ExprLens.lean chore: code convention (#4009) 2024-04-28 15:49:55 +00:00
ExprTraverse.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ForEachExpr.lean chore: avoid runtime array bounds checks (#6134) 2024-11-21 05:04:52 +00:00
FunInfo.lean feat: refactor of find functions on List/Array/Vector (#6833) 2025-01-30 01:14:21 +00:00
GeneralizeTelescope.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
GeneralizeVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
GetUnfoldableConst.lean perf: async optimizations for Init.Data.BitVec.Lemmas (#7546) 2025-03-18 12:56:16 +00:00
GlobalInstances.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
IndPredBelow.lean feat: deprecate Array.mkArray in favour of Array.replicate 2025-03-24 08:25:00 +01:00
Inductive.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InferType.lean perf: Environment blocker removals from async-proofs branch (#7483) 2025-03-14 13:37:01 +00:00
Injective.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
Instances.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
IntInstTesters.lean feat: divisibility constraint normalizer (#7092) 2025-02-15 04:20:40 +00:00
Iterator.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
KAbstract.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
KExprMap.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
LazyDiscrTree.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
LevelDefEq.lean chore: mark Meta.Context.config as private (#6051) 2024-11-13 13:30:06 +11:00
LitValues.lean doc: Char docstring proofreading (#7198) 2025-03-08 22:17:01 +00: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 feat: Nat divisibility constraints in cutsat (#7495) 2025-03-15 03:46:47 +00:00
Offset.lean chore: cleanup imports (#5825) 2024-10-23 23:51:13 +00:00
PPGoal.lean fix: have Lean.Meta.ppGoal use hard newlines (#5640) 2024-10-08 17:36:08 +00:00
PProdN.lean chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00
RecursorInfo.lean feat: refactor of find functions on List/Array/Vector (#6833) 2025-01-30 01:14:21 +00:00
Reduce.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ReduceEval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SizeOf.lean feat: deprecate Array.mkArray in favour of Array.replicate 2025-03-24 08:25:00 +01:00
Sorry.lean feat: labeled and unique sorries (#5757) 2024-12-11 23:53:02 +00:00
Structure.lean refactor: factor out common code for structure default values (#7737) 2025-03-31 22:40:39 +00:00
SynthInstance.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Tactic.lean feat: cutsat preparations (#7097) 2025-02-16 02:52:14 +00:00
Transform.lean feat: grind preprocessing and Expr internalization (#6413) 2024-12-19 00:16:48 +00:00
TransparencyMode.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
UnificationHint.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
WHNF.lean feat: zeta and zetaDelta options in grind (#7723) 2025-03-29 20:07:53 +00:00