-
Notifications
You must be signed in to change notification settings - Fork 1k
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Inconsistency in functions handling private names
bugSomething isn't workingSomething isn't workingStatus: Open.#15308 In leanprover/lean4;Anonymous instances are sometimes silently not created
bugSomething isn't workingSomething isn't workingStatus: Open.#15302 In leanprover/lean4;Type ascription with autoParam under ∀ᵐ times out
bugSomething isn't workingSomething isn't workingStatus: Open.#15284 In leanprover/lean4;- Status: Open.#15282 In leanprover/lean4;
- Status: Open.#15281 In leanprover/lean4;
- Status: Open.#15264 In leanprover/lean4;
grind with BitVec.allOnes is broken by replacing variable with literal constant
bugSomething isn't workingSomething isn't workingStatus: Open.#15261 In leanprover/lean4;grind_hom does not recognize arithmetic properties of constant bitmasks
bugSomething isn't workingSomething isn't workingStatus: Open.#15260 In leanprover/lean4;- Status: Open.#15246 In leanprover/lean4;
RFC: safe withExclusive wrapper around isExclusiveUnsafe
RFCRequest for commentsRequest for commentsStatus: Open.#15235 In leanprover/lean4;#print axioms/collectAxiomsunder-reports axioms of imported inductives (in-progress sentinel cached byexportedAxiomsExt)bugSomething isn't workingSomething isn't workingStatus: Open.#15226 In leanprover/lean4;@[deprecated]on a structure field projection does not warn when constructing the fieldbugSomething isn't workingSomething isn't workingStatus: Open.#15203 In leanprover/lean4;