max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Paul Reichert d4af4e26f9
feat: upstream Rat.abs and Int/Rat lemmas from human-eval-lean (#12412) 
This PR introduces `Rat.abs` and adds missing lemmas about `Int` and
`Rat`.

For `Int`:
- Lemmas about the interaction of negation and order: `neg_le_iff`,
`le_neg_iff`, `neg_lt_iff`, `lt_neg_iff`

For `Rat`:
- Declaration of `Rat.abs`
- Lemmas for `Rat.abs`, `Rat.floor` and `Rat.ceil`
- More basic lemmas that would all be provable with `grind` but might
still be good to have in the library
- Type class instances: `Std.Associative`, `Std.Commutative`,
`Std.LawfulIdentity` for addition
2026-02-11 11:07:08 +00:00
..
Control chore: missing annotations (#12368) 2026-02-09 04:52:13 +00:00
Data feat: upstream Rat.abs and Int/Rat lemmas from human-eval-lean (#12412) 2026-02-11 11:07:08 +00:00
Grind chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
GrindInstances feat: unfold [reducible] class fields (part 1) (#12340) 2026-02-06 16:18:33 +00:00
Internal chore: revert reducibility change PartialOrder.rel (#12407) 2026-02-10 19:46:36 +00:00
Meta chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Omega chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Sym chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
System feat: IO.FS.Metadata.numLinks (#12277) 2026-02-09 14:28:56 +00:00
BinderNameHint.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
BinderPredicates.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
ByCases.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Classical.lean feat: @[instance_reducible] part 2 (#12263) 2026-02-03 04:01:13 +00:00
Coe.lean doc: fix typo in Init.Coe module docstring (#11567) 2025-12-10 08:48:55 +00:00
Control.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Conv.lean feat: add experimental cbv tactic (#12279) 2026-02-04 14:39:39 +00:00
Core.lean chore: revert reducibility change to HasSSubset for now (#12403) 2026-02-10 06:33:38 +00:00
Data.lean chore: more reorganization of strings (#10928) 2025-10-23 11:56:11 +00:00
Dynamic.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Ext.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
GetElem.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Grind.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
GrindInstances.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Guard.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Hints.lean feat: some unification hints (#12341) 2026-02-09 04:51:13 +00:00
Internal.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
LawfulBEqTactics.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
MacroTrace.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Meta.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
MetaTypes.lean feat: do not simp instances (#12244) 2026-02-05 04:53:46 +00:00
MethodSpecsSimp.lean feat: @[method_specs_simp] in Init (#10407) 2025-09-16 10:27:33 +00:00
Notation.lean doc: add pp.mvars advice to #guard_msgs docstring (#12253) 2026-01-30 16:13:24 +00:00
NotationExtra.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Omega.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Prelude.lean feat: @[instance_reducible] part 2 (#12263) 2026-02-03 04:01:13 +00:00
PropLemmas.lean feat: more lemmas relating Bool and (d)ite (#12371) 2026-02-07 09:05:46 +00:00
RCases.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ShareCommon.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
SimpLemmas.lean feat: improves simpArrowTelescope simproc (#12153) 2026-01-25 22:29:38 +00:00
Simproc.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
SizeOf.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
SizeOfLemmas.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Sym.lean feat: add Sym.Simp.evalGround simproc (#12031) 2026-01-17 05:13:12 +00:00
Syntax.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
System.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Tactics.lean feat: add decide_cbv tactic (#12411) 2026-02-11 10:12:23 +00:00
TacticsExtra.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Task.lean chore: shake core (#12276) 2026-02-05 09:10:32 +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 chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
WFComputable.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
WFExtrinsicFix.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
WFTactics.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
While.lean fix: move the monad argument for ForIn, ForIn', and ForM (#10204) 2025-11-25 12:20:37 +00:00