Pedro Arêdes PHAredes

Prompt 2: Generate HTML from Markdown Resume (English)

This prompt remains the same as before, as it's designed to take any Markdown resume and apply consistent styling.

You are an expert web developer specializing in clean, modern, and print-friendly HTML and CSS.
My goal is to convert a given resume in Markdown format into a single HTML file that is well-structured, responsive, and easy to extract into a PDF.

O interpreter usa:

Variáveis localmente anônimas (elas ganham um "nome" durante a aplicação)
Call-by-name, com uma semântica operativa de redução
Normalização completa (a redução continua dentro dos lambdas)
Consideramos para a redução termos fechados e um subset dos termos abertos (o suficiente para representar e computar os combinadores BCKI, o que permite representar termos afins)

Some fixite for the binary relations

infixl 3 _⋈_ -- context split
infix  4  _⊢_ -- scope judgement
infix  4  _∈_ -- context membership (left associative)
infixl 5  _,_ -- context snoc (right associative cons)

We need the ℕ numbers type:

(find-firefox "https://agda.readthedocs.io/en/v2.6.1/language/rewriting.html#general-shape-of-rewrite-rules")
(find-firefox "https://jesper.sikanda.be/posts/hack-your-type-theory.html")
(find-firefox "https://jesper.sikanda.be/posts/agdas-new-sorts.html")
(find-wget-elisp "https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/src/Relation/Binary/PropositionalEquality/Core.agda")
(find-wget-elisp "https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/src/Data/Vec/Base.agda")

Boilerplate

Setting the options to allow rewriting macros and disable K axiom (not used here)

	-- This is an extension on the Oleg implementation of PHOAS NbE
	-- to support builtin natural numbers, products and general recursion via fixed-points
	-- https://oleg.fi/gists/posts/2025-02-11-nbe-phoas.html

	module PHOAS where

	open import Agda.Builtin.Sigma using (Σ; _,_)
	open import Agda.Builtin.Nat renaming (Nat to ℕ)

	module Lib where

	{-# OPTIONS --guardedness #-}

	open import IO
	open import Data.Unit.Polymorphic
	open import Level
	open import Data.Bool
	open import Data.String
	using (String; _==_; show; fromList)
	renaming (_++_ to _++s_)
	open import Data.Maybe

	open import Agda.Primitive using () renaming (lzero to l0)
	open import Induction.WellFounded using (Acc; acc)
	open import Relation.Binary.Construct.Closure.Transitive
	open import Relation.Binary.PropositionalEquality
	open import Data.Empty using (⊥-elim)
	open import Relation.Binary using (Rel)
	open import Function using (flip)
	open import Data.Nat renaming (ℕ to Nat)
	open import Data.Nat.Properties
	open import Data.Nat.Induction using (<-wellFounded)

	{-# OPTIONS --cubical-compatible --safe --erasure #-}

	module Affine where

	open import Level renaming (suc to lsuc; zero to lzero)
	open import Data.Nat renaming (ℕ to Nat)
	open import Data.Nat.Properties
	open import Data.Product
	open import Data.List
	open import Data.Empty

	{-# OPTIONS --cubical --safe #-}
	open import Cubical.Foundations.Prelude
	open import Cubical.Data.Nat.Order
	open import Cubical.Data.Sigma
	open import Cubical.Data.Nat renaming (ℕ to Nat)
	open import Cubical.Data.Empty renaming (elim to ⊥-elim; rec to ⊥-rec)
	open import Cubical.Relation.Nullary
	open import Cubical.Relation.Binary
	open import Algebra
	open import Level using (Level) renaming (_⊔_ to l-max; suc to lsuc)

	{-# OPTIONS --cubical #-}

	open import Cubical.Core.Primitives
	open import Cubical.Core.Glue
	open import Cubical.Data.Sigma
	open import Cubical.Data.Nat renaming (ℕ to Nat)
	open import Cubical.Data.Vec
	open import Cubical.Foundations.Equiv
	open import Cubical.Foundations.Transport
	open import Cubical.Foundations.Equiv