Search results

[Unsupported Rust] Let chains

unsupported-rustRust code rejected by hax. Unless marked wontfix, we want to support it soon.Rust code rejected by hax. Unless marked wontfix, we want to support it soon.

Status: Open.

#2018 In cryspen/hax;

· maximebuyse opened on Apr 23, 2026

[Frontend] Could not find a clause for binder on type alias

Status: Open.

#2017 In cryspen/hax;

· maximebuyse opened on Apr 23, 2026

[Frontend] Bug with extraction of some serde derived impls in --experimental-full-def mode

Status: Open.

#2013 In cryspen/hax;

· maximebuyse opened on Apr 22, 2026

[F*] sealed trait pattern rejected as syntax error

Status: Open.

#2011 In cryspen/hax;

· redshiftzero opened on Apr 16, 2026

[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

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