Skip to content

Instantly share code, notes, and snippets.

David Thrane Christiansen david-christiansen

View GitHub Profile
david-christiansen /
Last active May 15, 2017
How to fix the audio on the current crop of OPLSS videos
for i in *.mp4; do
if [ ! -a "${i%.mp4}-fixed.mp4" ]; then
ffmpeg -i "$i" -vcodec copy -ac 1 "${i%.mp4}-fixed.mp4"
david-christiansen / monad-notation.rkt
Created Mar 23, 2016
Monad notation for Typed Racket
View monad-notation.rkt
#lang typed/racket
(require (for-syntax racket syntax/parse) racket/stxparam)
(provide do-impl define-do pure)
(module+ test (require typed/rackunit))
(define-syntax (<- stx) (raise-syntax-error '<- "used outside of do"))
View Main.idr
module Main
import Data.Vect
import Data.Fin
%default total
||| If a value is neither at the head of a Vect nor in the tail of
||| that Vect, then it is not in the Vect.
notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
View Monoid.idr
import Language.Reflection.Elab
namespace Tactics
||| Restrict a polymorphic type to () for contexts where it doesn't
||| matter. This is nice for sticking `debug` in a context where
||| Idris can't solve the type.
simple : {m : Type -> Type} -> m () -> m ()
simple x = x
View MTac.idr
syntax mmatch [t] as {x} returning [ty] cases [cs] =
Match (\x => ty) t cs
syntax pat {x} "." [tm] = PTele (\x => tm)
syntax [tm1] "=>" [tm2] = PBase tm1 tm2
foo : Tac (List ())
foo = mmatch Z as y returning (List ())
cases [
View STLC.idr
data Typ =
| BolTyp
| FunTyp Typ Typ
toType : Typ -> Type
toType IntTyp = Integer
toType BolTyp = Bool
toType (FunTyp x y) = toType x -> toType y
View NotElem.idr
module NotElem
import Language.Reflection.Elab
import Language.Reflection.Utils
import Data.List
emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible
View Schema.idr
data HList : List Type -> Type where
Nil : HList []
(::) : t -> HList ts -> HList (t :: ts)
%name HList xs,ys
append : HList ts -> HList ts' -> HList (ts ++ ts')
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
View Bin.idr
||| Binary parsing, based on the stuff in Power of Pi
module Bin
import System
import Data.So
import Data.Vect
import Bytes
View ClassNonsense.idr
module ClassNonsense
import Language.Reflection.Elab
class Foo t where
constructor MkFoo
foo : t
myFoo : Foo Nat
myFoo = MkFoo 1
You can’t perform that action at this time.