Expand description
Compute an ordering on declarations that:
- Detects mutually-recursive groups;
- Always orders an item before any of its uses (except for recursive cases);
- Otherwise keeps a stable order.
Aeneas needs this because proof assistant languages are sensitive to declaration order and need to be explicit about mutual recursion. This should come useful for translation to any other language with these properties.
Structs§
Enums§
- A (group of) top-level declaration(s), properly reordered.
- A (group of) top-level declaration(s), properly reordered. “G” stands for “generic”