BOOM Analytics: Exploring Data-Centric, Declarative Programming for the Cloud
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Sorting where | |
-- See https://www.twanvl.nl/blog/agda/sorting | |
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax) | |
open import Data.List hiding (merge) | |
open import Data.List.Properties | |
open import Data.Nat hiding (_≟_;_≤?_) | |
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans) | |
open import Data.Nat.Logarithm | |
open import Data.Nat.Induction |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Algorithm W (Damas-Hindley-Milner) in LiveScript. | |
# By Paul Miller (paulmillr.com), Public domain. | |
# | |
# Based on Robert Smallshire's [Python code](http://bit.ly/bbVmmX). | |
# Which is based on Andrew's [Scala code](http://bit.ly/aztXwD). | |
# Which is based on Nikita Borisov's [Perl code](http://bit.ly/myq3uA). | |
# Which is based on Luca Cardelli's [Modula-2 code](http://bit.ly/Hjpvb). | |
# Something like that. | |
prelude = require './prelude' |
There are so many great GIFs out there and I want to have copies of them. Twitter makes that harder than it should be by converting them to MP4 and not providing access to the source material. To make it easier, I made a bash pipeline that takes a tweet URL and a filename, extracts the MP4 from that tweet and uses ffmpeg to convert back to GIF.
- ffmpeg
- macOS:
brew install ffmpeg
- Ubuntu/Debian:
apt install ffmpeg
- macOS:
OlderNewer