Scope

ff-html-examples is a compact Agda companion library that exercises typed HTML and CSS construction through executable page examples. Its Showcase module defines reusable styles, selector-backed stylesheet data, document heads, and concrete pages ranging from an introduction and semantic article to a dashboard and component gallery. The Generate module renders safe HTML values into complete documents and invokes an external writer during type checking. HTML.Everything ties both modules into a single check surface, which the generated metadata records as three checked modules and 740 lines.

Most important results

The showcase assembles typed examples for tables, forms, media embeds, web-component templates, navigation, metrics, and cards into complete pages. It demonstrates both inline CSS values and a structured selector stylesheet, including a separately rendered stylesheet representation. Five named documents cover an introduction, a semantic article, selector styling, a dashboard, and a component gallery. The generation path accepts successful writer execution as a type-checking result and raises a detailed error containing the output path, standard output, standard error, and rendered input when writing fails.