jozefg

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

jozefg

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

#!/usr/bin/env python3
from datetime import date, timedelta
import argparse
import time
import itertools

import requests
import feedparser

OKBLUE = '\033[94m'

jozefg

;; 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)

jozefg

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)

jozefg

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

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 =

jozefg

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

jozefg

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

(* 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 ()