List view

proof-lib/lean Turn the prelude into a proper Lean package

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.

Task

#1663 In cryspen/hax;

· clementblaudeau opened on Sep 4, 2025

[Lean] Add missing cases for loops over all integer types

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

libLib-related issue (e.g. annotations lib)Lib-related issue (e.g. annotations lib)

P1Max priorityMax priority

Status: Open.

#1783 In cryspen/hax;

· clementblaudeau opened on Nov 26, 2025

[Lean] Add support for f16 and f128 floats

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

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.

#1787 In cryspen/hax;

· abentkamp opened on Dec 1, 2025

[Lean] Pattern-matching on float literals

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.

#1788 In cryspen/hax;

· abentkamp opened on Dec 1, 2025