Skip to content

Instantly share code, notes, and snippets.

View jonsterling's full-sized avatar

Jon Sterling jonsterling

802 followers · 368 following
View GitHub Profile
@jonsterling
jonsterling / NSMenuItem+RSCore.swift
Last active January 11, 2026 13:45 — forked from brentsimmons/NSMenuItem+RSCore.swift
Disable all menu item images in a Mac app.
//
// NSMenuItem+RSCore.swift
// RSCore
//
// Created by Brent Simmons on 1/5/26.
//
#if os(macOS)
import AppKit
import ObjectiveC
@jonsterling
jonsterling / exists.ml
Created March 17, 2016 15:14
existential quantifier in OCaml
(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
(* the predicate *)
type 'a phi
(* the existential type *)
type t
(* the introduction rule *)
@jonsterling
jonsterling / gist:5940947
Created July 6, 2013 19:23
Installing Idris / libffi on Mac OS 10.8
@jonsterling
jonsterling / STC.agda
Created February 26, 2021 02:54
STC.agda
{-# OPTIONS --type-in-type --cubical --rewriting --confluence-check #-}
module stc-playground where
open import Cubical.Foundations.Prelude
open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
open import Agda.Builtin.Equality.Rewrite
open import Agda.Primitive
@jonsterling
jonsterling / namespace.sty
Created September 3, 2020 17:31
\RequirePackage{expl3}
\RequirePackage{xparse}
\ProvidesExplPackage {namespace} {2020/08/31} {0.1} {Compositional namespaces for labels}
\tl_new:N \l_ns_stk
\cs_new:Npn \ns_push:n #1 {
\tl_put_right:Nn \l_ns_stk {#1}
\tl_put_right:Nn \l_ns_stk {/}
@jonsterling
jonsterling / GluedEval.hs
Created May 8, 2020 16:44 — forked from AndrasKovacs/GluedEval.hs
Non-deterministic normalization-by-evaluation in Olle Fredrikkson's flavor.
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
https://github.com/ollef/sixty
The main idea is that during elaboration, we need different evaluation
@jonsterling
jonsterling / jon-ebproof.sty
Created September 1, 2019 03:27
\RequirePackage{expl3}
\RequirePackage{xparse}
\RequirePackage{ebproof}
%% This package is an extension and modification of code by Emmanuel Beffara
\ExplSyntaxOn
\cs_new_protected:Npn \__formulas_split: {
$\hskip 1em plus 1fil$\displaystyle
@jonsterling
jonsterling / excerpt.tex
Last active December 1, 2018 02:47
\section{Focused Sequent Calculus}
Focused sequent calculus has several class of proposition\footnote{We are
writing $\Neg{a},\Pos{a}$ for negative and positive atoms respectively. You may
also see these written as $\Neg{P},\Pos{P}$.} and context. We summarize them
below, noting that $\Pos{\Omega}$ ranges over ordered lists, whereas $\Gamma$
ranges over multisets:
\begin{grammar}
negative & \Neg{A} &
@jonsterling
jonsterling / XeLaTeX-Article-Template.tex
Created February 21, 2010 19:38
%!TEX TS-program = xelatex
%!TEX encoding = UTF-8 Unicode
\documentclass[letterpaper, 12pt]{article}
\usepackage{amsmath,amsfonts,amssymb,fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setmainfont{Adobe Caslon Pro}
\title{\Large\sc title goes here}
\author{Jonathan M. Sterling}
@jonsterling
jonsterling / gist:6bed2d3327b83d071ab397d290b6e1db
Last active September 20, 2018 02:57
Core RedML is (so far) a one-sided, polarized L calculus in the style of Curien-Herbelin-Munch.
Lambda calculus can be compiled to Core RedML through a bunch of gnarly macros. For instance, the term
(((lam [x] (lam [y] (pair x y))) nil) nil)
should evaluate to a pair of nils. This term is compiled into Core RedML as the first stage of the following
computation trace, which shows how it computes to the desired pair.
State: (cut