Search results

[Lean] Ill-typed Lean output when unnecessarily passing a mutable reference

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1984 In cryspen/hax;

· abentkamp opened on Mar 10, 2026

[Lean] Passing arrays as slices

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1983 In cryspen/hax;

· abentkamp opened on Mar 10, 2026

Function with &mut return values just produces sorry and does not emit an error

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1978 In cryspen/hax;

· abentkamp opened on Mar 5, 2026

rust_primitives.unsize omitted when argument is &mut

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1977 In cryspen/hax;

· abentkamp opened on Mar 5, 2026

Core models calls the Debug trait method dbg_fmt instead of fmt

proof-libIssues related the backend-specific definitions (in the proof-lib folder)Issues related the backend-specific definitions (in the proof-lib folder)

Status: Open.

#1976 In cryspen/hax;

· abentkamp opened on Mar 5, 2026

[F*] Incompatibility with newer versions of F*

Status: Open.

#1975 In cryspen/hax;

· mnnielsen opened on Mar 4, 2026

hax 0.3.6 crashes on RPITIT

engineIssue in the engineIssue in the engine

Status: Open.

Bug

#1965 In cryspen/hax;

· cfm opened on Feb 24, 2026

[Lean] Incorrect placement of RustM.of_isOk in generated trait items

Status: Open.

#1964 In cryspen/hax;

· JuanCoRo opened on Feb 20, 2026

[Lean] Grind Linter

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

proof-libIssues related the backend-specific definitions (in the proof-lib folder)Issues related the backend-specific definitions (in the proof-lib folder)

Status: Open.

#1960 In cryspen/hax;

· abentkamp opened on Feb 18, 2026

[Lean] Custom purification proofs for for-loops

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1958 In cryspen/hax;

· abentkamp opened on Feb 18, 2026

·  

Lean backend v1.0

Specs for recursive functions

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

P1Max priorityMax priority

Status: Open.

#1957 In cryspen/hax;

· abentkamp opened on Feb 18, 2026

Wrong encoding of Rust unicode chars

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

bugSomething isn't workingSomething isn't working

coqCoq backendCoq backend

f*F* backendF* backend

Status: Open.

#1953 In cryspen/hax;

· maximebuyse opened on Feb 17, 2026