Skip to content

Instantly share code, notes, and snippets.


Daniel Gratzer jozefg

View GitHub Profile
View init-latex.el
;; 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)
View matchless-tail.agda
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)
View wf-too-strong.agda
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)
module Syn =
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 =
View howe.agda
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
View mltt.agda
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 /
Created Mar 21, 2018
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 ()
jozefg / intrinsic.agda
Last active Jan 12, 2018
Another formalization of "The intrinsic topology of a Martin-Lof Universe"
View intrinsic.agda
module intrinsic where
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum as S
open import Data.Bool as B
open import Data.Nat as N
open Cmdliner
module type Config_t =
type opt_level = O1 | O2 | O3
val int_of_opt : opt_level -> int
type config =
{ line_width : int
jozefg / pftools.sty
Created Oct 12, 2017
A handy package called pftools for LaTex.
View pftools.sty
\RequirePackage{\basedir locallabel}
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
You can’t perform that action at this time.