Tags: grunweg/batteries
Tags
chore: bump toolchain to v4.10.0-rc2 (leanprover-community#876)
chore: bump toolchain to v4.10.0-rc1, merging bump/v4.10.0 (leanprove… …r-community#867) * chore: adaptations for nightly-2024-06-11 (leanprover-community#837) * chore: adaptation for nightly-2024-06-14 (leanprover-community#845) * fix(linter): "(invalid MessageData.lazy, missing context)" (leanprover-community#838) * chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware (leanprover-community#839) * add test demonstrating undesired behaviour on dsimp lemmas * chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware * test demonstrates correct behaviour on dsimp lemmas * process review comments * make formatLemmas dsimp-aware * Revert "chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware (leanprover-community#839)" (leanprover-community#841) This reverts commit 007a82f. * feat: ext lemma for `Thunk` (leanprover-community#842) * chore: adaptations for nightly-2024-06-14 --------- Co-authored-by: L <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: François G. Dorais <[email protected]> * chore: adaptations for nightly-2024-06-16 (leanprover-community#848) * chore: adaptations for nightly-2024-06-19 (leanprover-community#855) * chore: adaptations for nightly-2024-06-22 (leanprover-community#856) * chore: bump toolchain to v4.10.0-rc1 * chore: adaptations for nightly-2024-06-30 (leanprover-community#866) * chore: bump toolchain to v4.10.0-rc1 * chore: adaptations for nightly-2024-06-30 * fix --------- Co-authored-by: L <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: François G. Dorais <[email protected]>
PreviousNext