Skip to content

Instantly share code, notes, and snippets.

View jozefg's full-sized avatar

daniel gratzer jozefg

View GitHub Profile
@jozefg
jozefg / cantor.agda
Created May 19, 2023 15:07
A generalization of Cantor's diagonalization argument.
module cantor where
open import Data.Product
open import Data.Empty
open import Level
-- A variant of (https://coq.inria.fr/refman/language/core/inductive.html?highlight=cantor)
-- Sort of spooky this works.
data _≡_ {ℓ : Level}{A : Set ℓ} : A A Set₀ where
refl : (a : A) a ≡ a
open import Data.Product
open import Relation.Binary.PropositionalEquality
singleton-contractible : {A : Set}(x : A) (p : Σ[ y ∈ A ] x ≡ y) (x , refl) ≡ p
singleton-contractible x ( .x , refl )= refl
transport : {A : Set}(B : A Set)(x y : A) x ≡ y B x B y
transport B x .x refl b = b
J : {A : Set}(B : (x y : A) x ≡ y Set) ((x : A) B x x refl) (x y : A)(p : x ≡ y) B x y p
@jozefg
jozefg / arxiv_scraper.py
Last active February 1, 2024 01:28
Query the arxiv api for latest articles in a given classification.
#!/usr/bin/env python3
from datetime import date, timedelta
import argparse
import time
import itertools
import requests
import feedparser
OKBLUE = '\033[94m'
;; auctex is under the name auctex on elpa but provides
;; the symbol tex. No clue why..
(require-package 'auctex 'tex)
(require-package 'reftex)
(require-package 'auctex-latexmk)
(setq TeX-auto-save t)
(setq TeX-parse-self t)
(setq-default TeX-engine 'default)
(add-hook 'LaTeX-mode-hook 'turn-on-reftex)
module matchless-tail where
data : Set where
zero :
suc :
data Vec (A : Set) : Set where
nil : Vec A zero
cons : {n} A Vec A n Vec A (suc n)
module wf-too-strong where
open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≟_)
open import Data.Nat.Properties using (≤-antisym; ≤-refl; ≤-step)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
@jozefg
jozefg / nbe.ml
Last active March 20, 2021 00:13
module Syn =
struct
type uni_level = int
type t =
| Var of int (* DeBruijn indices for variables *)
| Nat | Zero | Suc of t | NRec of t * t * t * t
| Pi of t * t | Lam of t | Ap of t * t
| Uni of uni_level
| Subst of t * subst
and subst =
module howe where
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Product
import Data.Fin as F
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Nullary
module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
data Tm : Set where
var : {n} F.Fin n Tm n
@jozefg
jozefg / exceptional.ml
Created March 21, 2018 20:34
Some exceptional programs in OCaml
(* Stubs to let us pretend that OCaml is closer to our language *)
let free (x : 'a ref) = print_endline "Deallocating...."
let fork (f : unit -> 'a) : 'unit = f (); ()
(** Example 1: A finally combinator. Ensuring that a thunk is evaluated
* after another thunk regardless of the exceptions it raises
*)
let finally f g =
match f () with
| _ -> g ()