Search results

Custom setoid on lists cannot use the <code>\~~</code> notation.

Status: Open.

#352 In leanprover/cslib;

· ctchou opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#351 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#350 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#349 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#348 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#347 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

fix proof to work with backward.isDefEq.respectTransparency

Status: Open.

#346 In leanprover/cslib;

· github-actions opened on Feb 18, 2026

grind sets

Status: Open.

#308 In leanprover/cslib;

· chenson2018 opened on Jan 31, 2026

Automate <code>lake update</code> PRs

Status: Open.

#294 In leanprover/cslib;

· chenson2018 opened on Jan 26, 2026

move meta sections into new files

Status: Open.

#264 In leanprover/cslib;

· chenson2018 opened on Jan 12, 2026

enable module-aware shake in CI

Status: Open.

#263 In leanprover/cslib;

· chenson2018 opened on Jan 12, 2026

<code>grind</code> does not use congruence relations with <code>na.totalize.MTr</code>

Status: Open.

#253 In leanprover/cslib;

· github-actions opened on Jan 9, 2026