-
Notifications
You must be signed in to change notification settings - Fork 932
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Document or expose the Std.Internal.Do entry point required by vcgen
bugSomething isn't workingSomething isn't workingStatus: Open.#14762 In leanprover/lean4;lake cache get fails a whole batch after one transient network failure
bugSomething isn't workingSomething isn't workingStatus: Open.#14739 In leanprover/lean4;Unknown constant error for privately imported unification hint
bugSomething isn't workingSomething isn't workingStatus: Open.#14734 In leanprover/lean4;Crash on overapplication of Quot.mk or trivial structures
bugSomething isn't workingSomething isn't workingStatus: Open.#14719 In leanprover/lean4;variablemay cause sorrybugSomething isn't workingSomething isn't workingStatus: Open.#14718 In leanprover/lean4;- Status: Open.#14715 In leanprover/lean4;
Autoparam helper decls are always private
bugSomething isn't workingSomething isn't workingStatus: Open.#14708 In leanprover/lean4;repeatwith a missing body burns the full heartbeat budget and ~4 GB on a file after a parse error has already been reportedbugSomething isn't workingSomething isn't workingStatus: Open.#14704 In leanprover/lean4;Lean.version.specialDesc is inconsistent between platforms on recent nightlies
bugSomething isn't workingSomething isn't workingStatus: Open.#14702 In leanprover/lean4;interpreter error from
import all+public importallowing non-meta private def in public meta defbugSomething isn't workingSomething isn't workingStatus: Open.#14697 In leanprover/lean4;choice nodes are mishandled in tactic and command elaboration
bugSomething isn't workingSomething isn't workingStatus: Open.#14695 In leanprover/lean4;Formatter emits trailing whitespace before multi-tactic
tacticSeqargumentsbugSomething isn't workingSomething isn't workingStatus: Open.#14692 In leanprover/lean4;