Skip to content

Use a resugaring to identify literal consts #1614

@clementblaudeau

Description

@clementblaudeau

The lean backend directly matches on the body of items to identify constants that do not require the monadic encoding. It should be done properly with a resugaring instead.

Metadata

Metadata

Labels

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

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions