Skip to content

Instantly share code, notes, and snippets.

View paldepind's full-sized avatar

Simon Friis Vindum paldepind

View GitHub Profile
@paldepind
paldepind / keybase.md
Created March 4, 2024 07:58
Keybase proof

Keybase proof

I hereby claim:

  • I am paldepind on github.
  • I am paldepind (https://keybase.io/paldepind) on keybase.
  • I have a public key ASD8KH9Ww6dB3tn7d8hJkbL3zhgaChfCqHn-T7JnVfjThgo

To claim this, I am signing this object:

import 'package:flutter/material.dart';
void main() => runApp(const LogoApp());
double? first = null;
class AnimatedLogo extends AnimatedWidget {
const AnimatedLogo({super.key, required Animation<double> animation})
: super(listenable: animation);
@paldepind
paldepind / main.dart
Created November 12, 2023 12:41
Material dark mode
import 'package:flutter/material.dart';
void main() => runApp(TestApp());
class TestApp extends StatelessWidget {
@override
Widget build(BuildContext context) {
return MaterialApp(
home: Theme(
data: ThemeData(brightness: Brightness.dark),
@paldepind
paldepind / main.dart
Created November 12, 2023 12:35
Cupertino dark theme
import 'package:flutter/cupertino.dart';
void main() => runApp(TestApp());
class TestApp extends StatelessWidget {
@override
Widget build(BuildContext context) {
return const CupertinoApp(
home: CupertinoTheme(
data: CupertinoThemeData(brightness: Brightness.dark),
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 October 3, 2020 17:09
Positive fractions where 1 = 1/2 + 1/2 holds by reflexivity.
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
}.
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);
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 March 16, 2017 13:38
Player timeline implemented in Funnel
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 September 19, 2016 11:10
requirebin sketch
// 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)