A dependently typed domain-specific language for hardware design, embedded into Agda.