G. Allais

Cf. how it's implemented in Idris: https://github.com/idris-lang/Idris2/blob/main/src/Idris/SetOptions.idr#L187-L189

1. Preliminary work detecting remarkable gates (zero, not, nand, and, or) 2. Simplifications involving negation 3. Deadcode elimination

This would allow us to write arithmetic circuits that are shown to respect place values

This would allow us to quickly show how circuits are generated from tables. Bonus point for exploiting symmetries.

This would allow us to quickly generate transformed circuits demonstrating the impact of DM on e.g. circuit latency.

This should allow us to highlight code

Allow DISPLAY to check whether a lambda is constant

3

As suggested by @mietek: it would be nice to be able to declare DISPLAY rules for the special case where a function is constant. For instance: ```agda open import Agda.Builtin.Sigma...

Found by @bishboria: when you want to refold a projection out of a specific record to the name it was given, Agda understands the record's name as a mere variable...

Known issues of the `--mkdoc` command

2

In case people want to have a look, the bulk of the command is implemented in `Idris.Doc.String` (for the `:doc` command that the `--mkdoc` command reuses) and `Idris.Doc.HTML`. Copy/pasted from...