All issues

Search results

Lean's Inhabited cannot be faithfully imported when instantiated at Prop (mapped to SProp)

Status: Open.

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

· ebmoon opened on Apr 21, 2026

Supporting version 2?

Status: Open.

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

· JasonGross opened on Dec 27, 2025

File "./imported.v", line 2, characters 0-51: Error: Error at line 43527 (for Quot.liftOn): #DEF 3090 39596 39609 30 90 missing Quot

Status: Open.

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

· JasonGross opened on Dec 23, 2025

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 conversion 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