Search results

Tiers of edits

Status: Open.

#224 In plclub/hs-to-rocq;

· lastland opened on Apr 23, 2026

Support for Rocq 9.0

Status: Open.

#220 In plclub/hs-to-rocq;

· lastland opened on Apr 2, 2026

Data/Functor/Classes: can't regenerate (GHC 9.10 quantified superclass)

blocked-dependencyBlocked by axiomatized or unavailable dependenciesBlocked by axiomatized or unavailable dependencies

tool-improvementImprovements to the hs-to-coq translatorImprovements to the hs-to-coq translator

Status: Open.

#217 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

GHC: FloatIn/FloatOut/OccurAnal fully axiomatized

enhancementNew feature or requestNew feature or request

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#216 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

Containers: 2 Admitted (restrictKeys, isProperSubsetOf) close to done

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#215 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

IntSetWordProofs.v: ~80 Admitted, needs bounded Word model

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#214 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

CSE.v: 5 Admitted, regression from axiomatized cseExpr in GHC 9.10

blocked-dependencyBlocked by axiomatized or unavailable dependenciesBlocked by axiomatized or unavailable dependencies

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#213 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

TrieMap.v: 5 Admitted TrieMapLaws instances

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#212 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

VarSetFSet.v: 9 Admitted, stub implementations block 5 proofs

enhancementNew feature or requestNew feature or request

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#211 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

Exitify.v: 3 Admitted, regression from GHC 9.10 type changes

proof-gapAdmitted or incomplete Coq proofsAdmitted or incomplete Coq proofs

Status: Open.

#210 In plclub/hs-to-rocq;

· lastland opened on Mar 24, 2026

Dockerfile

Status: Open.

#208 In plclub/hs-to-rocq;

· ivanperez-keera opened on Mar 20, 2025

add nix to ci

Status: Open.

#201 In plclub/hs-to-rocq;

· quinn-dougherty opened on Nov 3, 2021