Skip to content

Do not functionalize loops in the Lean backend, instead use Lean's for #1703

@clementblaudeau

Description

@clementblaudeau

As all rust computation is happening within a do block, we could use Lean for loops instead of translating them to Hax folds.

Metadata

Metadata

Labels

backendIssue in one of the backends (i.e. F*, Coq, EC...)engineIssue in the engineleanRelated to the Lean backend or library

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions