| .. |
|
AC
|
fix: ac_nf0, simp_arith: don't tempt the kernel to reduce atoms (#5708)
|
2024-10-16 08:52:58 +00:00 |
|
Grind
|
chore: fix spelling mistakes in src/Lean/Meta/ (#5436)
|
2024-09-23 23:09:14 +00:00 |
|
LinearArith
|
feat: rename Array.shrink to take, and relate to List.take (#5796)
|
2024-10-21 23:35:32 +00:00 |
|
Simp
|
chore: move MessageData.ofConstName earlier (#5877)
|
2024-10-29 21:23:51 +00:00 |
|
AC.lean
|
perf: add prelude to all Lean modules
|
2024-02-18 14:55:17 -08:00 |
|
Acyclic.lean
|
fix: regression on match expressions with builtin literals (#3521)
|
2024-02-27 18:49:44 +00:00 |
|
Apply.lean
|
chore: add missing deprecation dates (#5884)
|
2024-10-30 05:37:36 +00:00 |
|
Assert.lean
|
feat: allow MVarId.assertHypotheses to set BinderInfo/Kind (#5587)
|
2024-10-02 05:09:49 +00:00 |
|
Assumption.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
AuxLemma.lean
|
feat: propagate maxHeartbeats to kernel (#4113)
|
2024-05-09 17:44:19 +00:00 |
|
Backtrack.lean
|
chore: rename List.join to List.flatten
|
2024-10-14 22:28:12 +11:00 |
|
Cases.lean
|
chore: fix spelling mistakes in src/Lean/Meta/ (#5436)
|
2024-09-23 23:09:14 +00:00 |
|
Cleanup.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Clear.lean
|
feat: variant of MVarId.tryClearMany (#5588)
|
2024-10-02 05:26:40 +00:00 |
|
Congr.lean
|
perf: add prelude to all Lean modules
|
2024-02-18 14:55:17 -08:00 |
|
Constructor.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Contradiction.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Delta.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
ElimInfo.lean
|
refactor: more idiomatic syntax for if h: (#5567)
|
2024-10-01 15:23:54 +00:00 |
|
FunInd.lean
|
fix: FunInd: withLetDecl and mkLetVar don’t mix (#5803)
|
2024-10-22 10:15:14 +00:00 |
|
FVarSubst.lean
|
perf: add prelude to all Lean modules
|
2024-02-18 14:55:17 -08:00 |
|
Generalize.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
Grind.lean
|
feat: add grind core module (#4249)
|
2024-05-22 03:50:36 +00:00 |
|
IndependentOf.lean
|
chore: upstream solve_by_elim (#3408)
|
2024-02-21 01:16:04 +00:00 |
|
Induction.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Injection.lean
|
fix: regression on match expressions with builtin literals (#3521)
|
2024-02-27 18:49:44 +00:00 |
|
Intro.lean
|
chore: make getIntrosize public (#5727)
|
2024-10-16 02:35:12 +00:00 |
|
LibrarySearch.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
LinearArith.lean
|
perf: add prelude to all Lean modules
|
2024-02-18 14:55:17 -08:00 |
|
NormCast.lean
|
feat: use attribute command to add and erase simprocs (#3511)
|
2024-02-26 23:41:49 +00:00 |
|
Refl.lean
|
feat: apply_rfl tactic: handle Eq, HEq, better error messages (#3714)
|
2024-09-20 08:25:10 +00:00 |
|
Rename.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Repeat.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
Replace.lean
|
chore: remove >6 month deprecations (#5199)
|
2024-08-29 05:18:44 +00:00 |
|
Revert.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
|
Rewrite.lean
|
chore: cleanup after export Bool.and/or/not/xor
|
2024-09-16 12:45:51 +10:00 |
|
Rewrites.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
Rfl.lean
|
refactor: back rfl tactic primarily via apply_rfl (#3718)
|
2024-09-25 10:34:42 +00:00 |
|
Simp.lean
|
feat: report diagnostic information for simp at exception
|
2024-05-01 03:19:39 +02:00 |
|
SolveByElim.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
Split.lean
|
fix: improve split discriminant generalization strategy (#4401)
|
2024-06-07 21:35:09 +00:00 |
|
SplitIf.lean
|
chore: remove SplitIf.ext cache (#5571)
|
2024-10-17 09:36:00 +00:00 |
|
Subst.lean
|
chore: fix spelling mistakes in src/Lean/Meta/ (#5436)
|
2024-09-23 23:09:14 +00:00 |
|
Symm.lean
|
chore: update copyrights (#5449)
|
2024-09-24 05:27:53 +00:00 |
|
TryThis.lean
|
feat: options pp.mvars.anonymous and pp.mvars.levels (#5711)
|
2024-10-14 21:44:15 +00:00 |
|
Unfold.lean
|
feat: let unfold do zeta-delta reduction of local definitions (#4834)
|
2024-09-07 21:48:08 +00:00 |
|
UnifyEq.lean
|
chore: move MessageData.ofConstName earlier (#5877)
|
2024-10-29 21:23:51 +00:00 |
|
Util.lean
|
chore: delete deprecations from 2022 (#4618)
|
2024-07-02 03:47:33 +00:00 |
