Skip to content

Instantly share code, notes, and snippets.

Jonathan Sterling jonsterling

Block or report user

Report or block jonsterling

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View jon-ebproof.sty
\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
View excerpt.tex
\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} &
View gist:6bed2d3327b83d071ab397d290b6e1db
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
View gist:2945940f555a37cc9349e79def330647
Flat profile:
Each sample counts as 0.01 seconds.
% cumulative self self total
time seconds seconds calls ms/call ms/call name
25.18 1.76 1.76 2415 0.73 0.85 mark_slice
10.44 2.49 0.73 4193520 0.00 0.00 camlHashtbl__insert_bucket_1371
9.87 3.18 0.69 6306936 0.00 0.00 camlHashtbl__add_1385
7.73 3.72 0.54 67916414 0.00 0.00 caml_page_table_lookup
5.87 4.13 0.41 4771 0.09 0.21 caml_empty_minor_heap
@jonsterling
jonsterling / LabelledAdd1.agda
Created May 13, 2018 — forked from larrytheliquid/LabelledAdd1.agda
Labelled types demo ala "The view from the left" by McBride & McKinna. Labels are a cheap alternative to dependent pattern matching. You can program with eliminators but the type of your goal reflects the dependent pattern match equation that you would have done. Inductive hypotheses are also labeled, and hence you get more type safety from usin…
View LabelledAdd1.agda
open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where
----------------------------------------------------------------------
add : (m n : ℕ) "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)
View new-mlton-results.txt
[0.066684s] Checked test/success/V-types.prl
[0.022747s] Checked test/success/bool-fhcom-without-open-eval.prl
[0.009820s] Checked test/success/bool-pair-test.prl
[0.010696s] Checked test/success/dashes-n-slashes.prl
[0.009144s] Checked test/success/decomposition.prl
[0.006263s] Checked test/success/discrete-types.prl
[0.013531s] Checked test/success/empty.prl
[0.009508s] Checked test/success/equality-elim.prl
[0.017783s] Checked test/success/equality.prl
[0.017168s] Checked test/success/fcom-types.prl
View LOL.v
This file has been truncated, but you can view the full file.
Nuprl_functional =
λ _top_assumption_ : nat,
(λ (_evar_0_ : (λ n : nat, matrix_functional (Nuprl n)) 0)
(_evar_0_0 : ∀ n : nat, (λ n0 : nat, matrix_functional (Nuprl n0)) (S n)),
match
_top_assumption_ as n
return ((λ n0 : nat, matrix_functional (Nuprl n0)) n)
with
View recitation-source.tex
\documentclass{article}
\usepackage{libertine}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{amsmath, amssymb, proof, microtype, hyperref}
\usepackage{mathpartir} % for mathpar, not for proofs
\usepackage{perfectcut}
\newcommand\Parens[1]{\perfectparens{#1}}
\newcommand\Squares[1]{\perfectbrackets{#1}}
View gist:486673f7943f5ddce7c68d2389341f90
module experiment where
open import Agda.Primitive
open import Prelude.List
open import Prelude.Size
open import Prelude.Monoidal
open import Prelude.Monad
open import Prelude.Functor
open import Prelude.Natural
open Size using (∞)
View lambda-nu.clf
id : type.
id/z : id.
id/s : id -o id.
answer : type.
yes : answer.
no : answer.
id/eq? : id -> id -> answer -> type.
id/eq/z/z : id/eq? id/z id/z yes.
You can’t perform that action at this time.