Search results

leanittest_complete_trailing_period.lean test fails (99% tests passed, 1 tests failed out of 1441)

Status: Open.

#816 In leanprover-community/lean;

· barracuda156 opened on Sep 3, 2024

Segmentation fault when using <code>get_env</code> with <code>run_tactic</code>

Status: Open.

#803 In leanprover-community/lean;

· lenianiva opened on Mar 15, 2023

"Invalid return type" error when definining inductive propositions can be attached to more suitable text range

Status: Open.

#802 In leanprover-community/lean;

· ddrone opened on Feb 25, 2023

pp.links handles unit.star badly

Status: Open.

#789 In leanprover-community/lean;

· eric-wieser opened on Dec 2, 2022

opening a namespace can affect elaboration

Status: Open.

#776 In leanprover-community/lean;

· alexjbest opened on Oct 26, 2022

local notation can change explicitness of arguments

bugSomething isn't workingSomething isn't working

Status: Open.

#772 In leanprover-community/lean;

· fpvandoorn opened on Sep 26, 2022

clang prints warnings: use reference type ... to prevent copying

Status: Open.

#767 In leanprover-community/lean;

· yurivict opened on Sep 5, 2022

Simple programs run for many seconds

Status: Open.

#765 In leanprover-community/lean;

· yurivict opened on Sep 1, 2022

Failures in get_peak_rss() should fail the application instead of silently returning 0

Status: Open.

#763 In leanprover-community/lean;

· yurivict opened on Aug 31, 2022

Kernel failed to type-check due to name collision involving <code>include</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#751 In leanprover-community/lean;

· Vierkantor opened on Jul 29, 2022

exceptions when saving oleans are not user-visible

Status: Open.

#750 In leanprover-community/lean;

· collares opened on Jul 29, 2022

<code>is_bi_equal</code> use of BinderInfo-unaware hashes causes many collisions (a.k.a. timeout when saving oleans)

Status: Open.

#749 In leanprover-community/lean;

· collares opened on Jul 29, 2022