Modern type-theory-based proof assistants/languages are increasingly supporting general-purpose programming, making them both practical and formally rigorous. This dual nature aligns well with the needs of safety-critical embedded system design. It is hence promising that such a language can be employed as a proper meta-language for building an embedded system design framework that integrates reasoning and programming. In this paper, we demonstrate a unified framework for synchronous embedded system design, which leverages both aspects of the quantitatively typed language Idris2, with a focus on an embedded domain-specific language (EDSL), named SynQ, in the framework. Specifically, we show that the leveraging of the expressiveness of quantitative type theory and the tagless final embedding allows synchronous systems to be properly modelled by SynQ. This then enables a systematic usage of Idris2 for facilitating both design and verification of synchronous systems, demonstrating an initial step towards a correct-by-construction embedded system design process.