Skip to content

Instantly share code, notes, and snippets.

Avatar

Simon Friis Vindum paldepind

View GitHub Profile
View intuit_to_spatial.v
From iris.bi Require Import bi.
Import bi.
From iris.proofmode Require Import tactics environments intro_patterns monpred.
Section intuit_to_spatial.
Context {PROP : bi}.
Implicit Types Γ Γp Γs : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
@paldepind
paldepind / qp.v
Last active Oct 3, 2020
Positive fractions where 1 = 1/2 + 1/2 holds by reflexivity.
View qp.v
From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option numbers.
(* Strictly positive rationals *)
(* Positive fractions. *)
Record Qpos : Set := mk_Qpos {
Qpos_num : positive;
Qpos_den : positive
}.
View move-script.js
const fs = require("fs");
const bundle = fs.readFileSync("path-to-webpack-bundle.html", "utf8");
const escaped = JSON.stringify(bundle);
const js = `export default ${escaped}`;
fs.writeFileSync("javascript-output-file.ts", js);
View experiment.purs
module Experiment
( mapHeterogenousRecord
, mapRecordBuilder
, class MapRecord
) where
import Prelude
import Prim.Row as Row
import Prim.RowList as RL
@paldepind
paldepind / player-timeline.ts
Created Mar 16, 2017
Player timeline implemented in Funnel
View player-timeline.ts
const model = (animation: Animation) => fgo(function* model({ playPauseS, replayS }: ToModel) {
const playingB: Behavior<boolean> = yield sample(scan((_, b) => !b, false, playPauseS));
const playingSpeedB = map((b) => b ? 1 : 0, playingB);
const initialTimeB = yield sample(integrate(playingSpeedB));
const positionB = yield sample(switcher(initialTimeB, snapshot(integrate(playingSpeedB), replayS)));
return [{ positionB, playingB }, {}];
});
const view = ({ playingB, positionB }: ToView): any => [
button({output: {click: "playPauseS"}}, icon(playingB.map((b) => b ? "pause" : "play_arrow"))),
@paldepind
paldepind / index.js
Created Sep 19, 2016
requirebin sketch
View index.js
// Welcome! require() some modules from npm (like you were using browserify)
// and then hit Run Code to run your code on the right side.
// Modules get downloaded from browserify-cdn and bundled in your browser.
let {addIndex, chain, curry, map, range} = require("ramda")
let snabbdom = require("snabbdom")
let h = require("snabbdom/h")
let hh = require("hyperscript-helpers")
let {div, span} = hh(h)
@paldepind
paldepind / index.js
Created Sep 7, 2016
requirebin sketch
View index.js
// Welcome! require() some modules from npm (like you were using browserify)
// and then hit Run Code to run your code on the right side.
// Modules get downloaded from browserify-cdn and bundled in your browser.
var patch = require('snabbdom').init([
require('snabbdom/modules/attributes'),
]);
var h = require('snabbdom/h');
var elem = h('div', [
@paldepind
paldepind / record.sh
Created Mar 17, 2016
Record a selected window to a gif file. Remove `-draw_mouse 0` if you want the cursor included.
View record.sh
#!/bin/bash
TMP_AVI=$(mktemp /tmp/outXXXXXXXXXX.avi)
ffcast -w % ffmpeg -y -f x11grab -draw_mouse 0 -show_region 1 -framerate 15 \
-video_size %s -i %D+%c -codec:v huffyuv \
-vf crop="iw-mod(iw\\,2):ih-mod(ih\\,2)" $TMP_AVI \
&& convert -set delay 10 -layers Optimize $TMP_AVI out.gif
@paldepind
paldepind / form.hs
Last active Feb 5, 2016
Helper function for creating forms in Reflex. The default of forms is prevented. A submit event and child is returned.
View form.hs
import GHCJS.DOM.EventM (event, preventDefault)
import GHCJS.DOM.Element
form :: MonadWidget t m => m a -> m (Event t (), a)
form child = do
(form, ch) <- el' "form" child
submit <- wrapDomEvent (_el_element form) elementOnsubmit (void $ preventDefault)
performEvent_ (return () <$ submit)
return (submit, ch)
@paldepind
paldepind / script.js
Created Feb 7, 2015
Promise inside IndexedDB transactions test
View script.js
var openRequest = indexedDB.open("library");
openRequest.onupgradeneeded = function() {
// The database did not previously exist, so create object stores and indexes.
var db = openRequest.result;
var store = db.createObjectStore("books", {keyPath: "isbn"});
var titleIndex = store.createIndex("by_title", "title", {unique: true});
var authorIndex = store.createIndex("by_author", "author");
// Populate with initial data.