max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Rob23oba b919cfff30
fix: public section in Dyadic files (#12199) 
This PR fixes `Init.Data.Dyadic.Instances` and `Init.Data.Dyadic.Inv`.
Previously, all declarations defined in boths file were private and not
exposed.
2026-01-29 03:05:43 +00:00
..
Control style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Data fix: public section in Dyadic files (#12199) 2026-01-29 03:05:43 +00:00
Grind feat: String and Char simprocs for SymM (#12077) 2026-01-21 00:05:40 +00:00
GrindInstances feat: improves Fin n support in grind (#11319) 2025-11-22 06:51:25 +00:00
Internal refactor: make CCPO class Prop-valued (#11425) 2025-12-04 13:33:36 +00:00
Meta chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
Omega chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00
Sym feat: String and Char simprocs for SymM (#12077) 2026-01-21 00:05:40 +00:00
System fix: use windows path separators in System.Uri.fileUriToPath? (#12197) 2026-01-28 09:10:34 +00:00
BinderNameHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
BinderPredicates.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
ByCases.lean chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00
Classical.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Coe.lean doc: fix typo in Init.Coe module docstring (#11567) 2025-12-10 08:48:55 +00:00
Control.lean feat: MonadAttach (#11532) 2025-12-16 18:57:00 +00:00
Conv.lean feat: add enter [in patt] syntax (#10081) 2025-08-23 17:16:53 +00:00
Core.lean feat: add DecidableEq instances for Sigma and PSimga (#12193) 2026-01-28 15:00:45 +00:00
Data.lean chore: more reorganization of strings (#10928) 2025-10-23 11:56:11 +00:00
Dynamic.lean perf: do not export opaque bodies (#10119) 2025-08-27 20:59:59 +00:00
Ext.lean chore: add deprecations for duplicated theorems (#10967) 2025-10-29 05:26:16 +00:00
GetElem.lean feat: another grind_pattern for getElem?_pos (#11963) 2026-01-28 03:45:54 +00:00
Grind.lean feat: Field norm num (#11350) 2025-11-25 19:47:31 +00:00
GrindInstances.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Guard.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Hints.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Internal.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
LawfulBEqTactics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MacroTrace.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Meta.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MetaTypes.lean chore: don't extract standalone constants as closed terms (#12027) 2026-01-16 14:52:14 +00:00
MethodSpecsSimp.lean feat: @[method_specs_simp] in Init (#10407) 2025-09-16 10:27:33 +00:00
Notation.lean fix: add syntax to recommended_spelling for inv (#12139) 2026-01-24 11:04:36 +00:00
NotationExtra.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Omega.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Prelude.lean perf: add introSubstEq shortcut (#12190) 2026-01-28 12:33:14 +00:00
PropLemmas.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
RCases.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ShareCommon.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
SimpLemmas.lean feat: improves simpArrowTelescope simproc (#12153) 2026-01-25 22:29:38 +00:00
Simproc.lean chore: more module system fixes and improvements from Mathlib porting (#10655) 2025-10-08 11:30:09 +00:00
SizeOf.lean chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
SizeOfLemmas.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Sym.lean feat: add Sym.Simp.evalGround simproc (#12031) 2026-01-17 05:13:12 +00:00
Syntax.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
System.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Tactics.lean chore: remove obsolete repeat macro 2026-01-28 16:27:57 +01:00
TacticsExtra.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Task.lean fix: revert the waitAny refactoring (#11000) 2025-10-29 08:27:16 +00:00
Try.lean feat: add first_par combinator for try? with grind +locals (#11949) 2026-01-09 21:09:41 +00:00
Util.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
WF.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
WFComputable.lean feat: port Batteries.WF for executable well-founded fixpoints (#11620) 2025-12-12 18:22:54 +00:00
WFExtrinsicFix.lean feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038) 2025-12-08 16:03:22 +00:00
WFTactics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
While.lean fix: move the monad argument for ForIn, ForIn', and ForM (#10204) 2025-11-25 12:20:37 +00:00