Skip to content

Generate structure-s for leaf cells #4732

@tothtamas28

Description

@tothtamas28

I.e. instead of

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

generate

structure SortGasCell : Type where
  val : SortGas

Due to circular dependencies between sorts, this is not straightforward. What can be attempted:

  1. Find the SCCs in the dependency graph of sorts (where sorts that map to an abbrev are represented by their parameter sorts (see step 3).
  2. Topologically sort the SCCs.
  3. Generate a mutual for each SCC, in topological order. For each sort that depends on a sort that maps to an abbrev, inline the abbrev's definition. This is necessary because an abbrev cannot be defined in the same mutual as inductive-s / structure-s.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions