//@ ignore-auxiliary (used by `./expansion-time.rs`)

1
2