-
Notifications
You must be signed in to change notification settings - Fork 945
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
unused argument causes
noncomputableerrorbugSomething isn't workingSomething isn't workingStatus: Open.#14894 In leanprover/lean4;Inductives with more than 1 constructor throw an error if "prelude" keyword is used
bugSomething isn't workingSomething isn't workingStatus: Open.#14887 In leanprover/lean4;- Status: Open.#14876 In leanprover/lean4;
Unsoundness: class inductive recursor can leak a private import and prove False
bugSomething isn't workingSomething isn't workingStatus: Open.#14875 In leanprover/lean4;lean_kernel_diag_is_enabled implementation has one stray *
bugSomething isn't workingSomething isn't workingStatus: Open.#14865 In leanprover/lean4;csimpandmacro_inlinecannot be arbitrarily nestedbugSomething isn't workingSomething isn't workingStatus: Open.#14859 In leanprover/lean4;lake crashes on macOS ARM64
bugSomething isn't workingSomething isn't workingStatus: Open.#14852 In leanprover/lean4;Lean.Meta.Sym.Simp.toHavereverses dependencies when reconstructinghavetelescopesbugSomething isn't workingSomething isn't workingStatus: Open.#14804 In leanprover/lean4;simp produces proof terms that lead to
(kernel) deterministic timeoutbugSomething isn't workingSomething isn't workingStatus: Open.#14803 In leanprover/lean4;- Status: Open.#14800 In leanprover/lean4;
- Status: Open.#14798 In leanprover/lean4;
autoTry.onSorrysuggests using the current theorem to solve the goalbugSomething isn't workingSomething isn't workingStatus: Open.#14792 In leanprover/lean4;