-
Notifications
You must be signed in to change notification settings - Fork 996
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
- 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;simpDiscrCtor?is broken in the presence of non-type parametersbugSomething isn't workingSomething isn't workingStatus: Open.#15200 In leanprover/lean4;#guard_msgshides error messages from commands outside of itbugSomething isn't workingSomething isn't workingStatus: Open.#15196 In leanprover/lean4;bv_decidefails withunknown free variable '_fvar.126'under certain contextsbugSomething isn't workingSomething isn't workingStatus: Open.#15195 In leanprover/lean4;