Skip to content

Instantly share code, notes, and snippets.

View PHAredes's full-sized avatar

Pedro Arêdes PHAredes

View GitHub Profile
-- 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
@PHAredes
PHAredes / resume-as-html.md
Created June 30, 2025 04:14
resume-prompt

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.
{-# 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
@PHAredes
PHAredes / ualc.lagda.md
Last active March 4, 2025 19:52
ualc, com explicações em pt e bugfixes

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)
@PHAredes
PHAredes / ualc-with-sn-proof.agda
Last active May 23, 2025 14:26
ualc interpreter (reduction semantics, singlestep, cbn) with strong normalization and termination proofs
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)

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:

@PHAredes
PHAredes / Affine.agda
Created December 14, 2024 22:27
Using dist and trichotomy to make substitution decidable
{-# 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
@PHAredes
PHAredes / int-as-setoid.agda
Last active December 4, 2024 17:47
Int quotient set (pair of Nats) as a setoid instead of a HIT
{-# 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)
@PHAredes
PHAredes / db.agda
Last active March 4, 2025 01:01
Back to extending Taelin/Oleg inspired interpreter
{-# 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