Search results

<code>omega</code> failing due to powers of numerals

bugSomething isn't workingSomething isn't working

Status: Open.

#9206 In leanprover/lean4;

· vasnesterov opened on Jul 5, 2025

LSP completions are not returned in a meaningful order

bugSomething isn't workingSomething isn't working

Status: Open.

#9192 In leanprover/lean4;

· gaearon opened on Jul 4, 2025

doc: mistake in <code>Option.getD</code> docString example

Status: Open.

#9189 In leanprover/lean4;

· Mal-Pat opened on Jul 4, 2025

bug: IR check in <code>compilerTest1.lean</code> fails

bugSomething isn't workingSomething isn't working

Status: Open.

#9186 In leanprover/lean4;

· datokrat opened on Jul 4, 2025

bug: using <code>private import</code> can lead to panic in downstream file

bugSomething isn't workingSomething isn't working

Status: Open.

#9185 In leanprover/lean4;

· datokrat opened on Jul 4, 2025

RFC: Add option to prevent arbitrary code execution in <code>TermElabM</code>

RFCRequest for commentsRequest for comments

Status: Open.

#9160 In leanprover/lean4;

· lenianiva opened on Jul 2, 2025

Fin.reverseInduction does not kernel reduce

bugSomething isn't workingSomething isn't working

Status: Open.

#9141 In leanprover/lean4;

· kckennylau opened on Jul 1, 2025

Instance synthesis sees through type synonyms

bugSomething isn't workingSomething isn't working

Status: Open.

#9077 In leanprover/lean4;

· sgouezel opened on Jun 29, 2025

RFC: Allow adjusting parameter binder explicitness in constructors

RFCRequest for commentsRequest for comments

Status: Open.

#9072 In leanprover/lean4;

· eric-wieser opened on Jun 29, 2025

Incorrect scoping in monadic <code>let mut</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#9037 In leanprover/lean4;

· mhuisi opened on Jun 27, 2025

RFC: Add <code>libidn2</code> support for Punycode Conversion in DNS Functions

RFCRequest for commentsRequest for comments

Status: Open.

#9036 In leanprover/lean4;

· algebraic-dev opened on Jun 27, 2025

RFC: Warn reverse FFI users who do not call <code>lean_setup_args</code>

RFCRequest for commentsRequest for comments

Status: Open.

#9034 In leanprover/lean4;

· TwoFX opened on Jun 27, 2025