Skip to content

[Lean] Do not ignore base expressions for constructors of structs #1637

New issue
New issue
Open
#1736
Open
[Lean] Do not ignore base expressions for constructors of structs#1637
#1736
Assignees
clementblaudeau
Labels
backendIssue in one of the backends (i.e. F*, Coq, EC...)easy-fixleanRelated to the Lean backend or library
Milestone
Lean backend v1.0
@clementblaudeau

Description

@clementblaudeau
clementblaudeau
opened on Sep 1, 2025

Probably an easy-fix, as Lean supports base expressions as well.

Metadata

Metadata

Assignees

Labels

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

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions