Skip to content

Instantly share code, notes, and snippets.

View jonsterling's full-sized avatar

Jon Sterling jonsterling

733 followers · 340 following
View GitHub Profile
@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 / LabelledAdd1.agda
Created May 13, 2018 15:52 — 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…
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 ∙ ε ∶ ℕ ⟩)
@jonsterling
jonsterling / Markdown.txt
Last active January 29, 2016 23:04 — forked from beckyconning/Markdown.md
discipline = __ (!`SELECT discipline FROM "/test/testDb/olympics" LIMIT 1`) year = __ (!`SELECT year FROM "/test/testDb/olympics" LIMIT 1`) country = {!`SELECT DISTINCT country FROM "/test/testDb/olympics"`} (!`SELECT country FROM "/test/testDb/olympics" LIMIT 1`) type = (!`SELECT DISTINCT type FROM "/test/testDb/olympics" LIMIT 1`) !`SELECT DISTINCT type FROM "/test/testDb/olympics" OFFSET 1` gender = [!`SELECT gender FROM "/test/testDb/olympics" LIMIT 1`] !`SELECT DISTINCT gender FROM "/test/testDb/olympics"`
@jonsterling
jonsterling / topology.v
Last active August 29, 2015 14:02 — forked from andrejbauer/topology.v
Require Import Coq.Unicode.Utf8.
Require Import List.
Global Obligation Tactic := compute; firstorder.
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
*)
@jonsterling
jonsterling / IBAForms.podspec
Created June 16, 2012 03:24 — forked from jk/IBAForms.podspec
Podspec for IBAForms
Pod::Spec.new do |s|
s.summary = 'A simple iPhone forms library'
s.license = 'Apache License, Version 2.0'
s.source = { :git => 'https://github.com/yardsale/IBAForms.git', :tag => '1.1.0' }
s.source_files = 'library/**/*.{h,m}'
s.author = { 'Itty Bitty Apps' => '[email protected]' }
s.version = '1.0.0'
s.homepage = 'https://github.com/ittybittydude/IBAForms'
s.name = 'IBAForms'
s.platform = :ios
@jonsterling
jonsterling / NSObject+BlockObservation.h
Created March 22, 2011 19:18 — forked from andymatuschak/NSObject+BlockObservation.h
//
// NSObject+BlockObservation.h
// Version 1.0
//
// Andy Matuschak
// [email protected]
// Public domain because I love you. Let me know how you use it.
//
typedef NSString AMBlockToken;
@jonsterling
jonsterling / BubbleView.h
Created January 16, 2011 23:52
//
// BubbleView.h
//
// Created by Josh Kendall on 12/28/10.
// Copyright 2010 JoshuaKendall.com. All rights reserved.
//
#import <UIKit/UIKit.h>
#import <QuartzCore/QuartzCore.h>
@jonsterling
jonsterling / shBrushRuby.js
Created January 13, 2011 08:39 — forked from robhurring/shBrushRuby.js
/**
* SyntaxHighlighter
* http://alexgorbatchev.com/
*
* SyntaxHighlighter is donationware. If you are using it, please donate.
* http://alexgorbatchev.com/wiki/SyntaxHighlighter:Donate
*
* @version
* 2.0.320 (May 03 2009)
*
@jonsterling
jonsterling / NSObject+PropertyDealloc.m
Created May 31, 2010 20:59 — forked from mkhl/NSObject+PropertyDealloc.m
// Author: Pierre Bernard, Jonathan Sterling
// Source: http://www.bernard-web.com/pierre/blog/index.php?id=2624434753771423706
// Caveat: Consider using http://github.com/andrep/RMModelObject instead.
@implementation NSObject (PropertyDealloc)
- (void)releaseProperties {
Class class = [self class];
unsigned int pCount;
objc_property_t *properties = class_copyPropertyList(class, &pCount);