Search results

feat: deprecated options

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 7969

#7969 In leanprover/lean4;

· nomeata opened on Apr 15, 2025

feat: Constructions for splitting and merging vectors of bitvectors

changelog-libraryLibraryLibrary

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the time

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Open (in progress).

leanprover/lean4number 7754

#7754 In leanprover/lean4;

· javra opened on Mar 31, 2025

feat: use <code>rfl</code> proofs of <code>Iff</code> in <code>dsimp</code>

breaks-mathlibThis is not necessarily a blocker for merging: but there needs to be a planThis is not necessarily a blocker for merging: but there needs to be a plan

release-ciEnable all CI checks for a PR, like is done for releasesEnable all CI checks for a PR, like is done for releases

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 3973

#3973 In leanprover/lean4;

· thorimur opened on Apr 23, 2024

fix: <code>isDefEq</code> handling of delayed-assigned mvars when <code>withAssignableSyntheticOpaque</code> is <code>true</code>

builds-mathlibCI has verified that Mathlib builds against this PRCI has verified that Mathlib builds against this PR

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 3473

#3473 In leanprover/lean4;

· thorimur opened on Feb 23, 2024

chore: upstream Std's linter framework

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Open (in progress).

leanprover/lean4number 3291

#3291 In leanprover/lean4;

· kim-em opened on Feb 9, 2024

feat: lake: <code>require</code> overhaul

builds-mathlibCI has verified that Mathlib builds against this PRCI has verified that Mathlib builds against this PR

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 3174

#3174 In leanprover/lean4;

· tydeu opened on Jan 13, 2024

feat: make constructor tactic fail in ambiguous cases

builds-mathlibCI has verified that Mathlib builds against this PRCI has verified that Mathlib builds against this PR

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 3127

#3127 In leanprover/lean4;

· hrmacbeth opened on Dec 31, 2023

feat: remove configuration olean on <code>lake clean</code>

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 2699

#2699 In leanprover/lean4;

· tydeu opened on Oct 16, 2023

feat: mark <code>rfl</code> proofs of <code>Iff</code> for use by <code>dsimp</code>

breaks-mathlibThis is not necessarily a blocker for merging: but there needs to be a planThis is not necessarily a blocker for merging: but there needs to be a plan

toolchain-availableA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNNA toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 2679

#2679 In leanprover/lean4;

· thorimur opened on Oct 12, 2023

feat: include <code>ppLine</code> in <code>many(1)Indent</code>

WIPThis is work in progress, and only a PR for the sake of CI or sharing. No review yet.This is work in progress, and only a PR for the sake of CI or sharing. No review yet.

Status: Draft (not ready).

leanprover/lean4number 2453

#2453 In leanprover/lean4;

· tydeu opened on Aug 23, 2023