Search results

Anomaly "Uncaught exception Invalid_argument("index out of bounds")."

Status: Open.

#49 In rocq-community/rocq-lean-import;

· JeffreyChang12 opened on Nov 25, 2025

Stack Overflow Error

Status: Open.

#48 In rocq-community/rocq-lean-import;

· JeffreyChang12 opened on Nov 25, 2025

Lean Import fails because unification fails to reduce enough

Status: Open.

#46 In rocq-community/rocq-lean-import;

· JasonGross opened on Nov 22, 2025

Consider using primitive rewrite rules to mimic Lean kernel's treatment of numerals

bugSomething isn't workingSomething isn't working

enhancementNew feature or requestNew feature or request

Status: Open.

#38 In rocq-community/rocq-lean-import;

· JasonGross opened on May 12, 2025

Declare implicit arguments

enhancementNew feature or requestNew feature or request

Status: Open.

#32 In rocq-community/rocq-lean-import;

· SkySkimmer opened on Mar 27, 2025

How much of mathlib4 can be ported to Coq using this?

Status: Open.

#29 In rocq-community/rocq-lean-import;

· ruplet opened on Mar 10, 2025

Use sort poly instead of duplicating definitions

Status: Open.

#13 In rocq-community/rocq-lean-import;

· SkySkimmer opened on Nov 6, 2023