-
Notifications
You must be signed in to change notification settings - Fork 957
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
stack overflow hangs instead of aborting when the fault lands inside the allocator
bugSomething isn't workingSomething isn't workingStatus: Open.#14992 In leanprover/lean4;olean loader: no-mmap fallback re-reads the entire file after the header probe
bugSomething isn't workingSomething isn't workingStatus: Open.#14991 In leanprover/lean4;Private proof materializes a public equation theorem
bugSomething isn't workingSomething isn't workingStatus: Open.#14986 In leanprover/lean4;substandsimpreorder hypotheses when rewritingbugSomething isn't workingSomething isn't workingStatus: Open.#14985 In leanprover/lean4;- Status: Open.#14977 In leanprover/lean4;
Unexpected compilation error "Could not find native implementation of external declaration"
bugSomething isn't workingSomething isn't workingStatus: Open.#14975 In leanprover/lean4;- Status: Open.#14973 In leanprover/lean4;
kernel rejects simp proof, dischargeEqnThmHypothesis not well behaving
bugSomething isn't workingSomething isn't workingStatus: Open.#14961 In leanprover/lean4;- Status: Open.#14958 In leanprover/lean4;
Cannot derive eq_def for an @[irreducible] well-founded definition
bugSomething isn't workingSomething isn't workingP-lowWe are not planning to work on this issueWe are not planning to work on this issueStatus: Open.#14957 In leanprover/lean4;Unification sees through type synonyms when checking instances' types
bugSomething isn't workingSomething isn't workingStatus: Open.#14949 In leanprover/lean4;RFC: Mutual inductives with heterogeneous universes
RFCRequest for commentsRequest for commentsStatus: Open.#14944 In leanprover/lean4;