david-christiansen

#!/bin/bash

for i in *.mp4; do
    if [ ! -a "${i%.mp4}-fixed.mp4" ]; then
       ffmpeg -i "$i" -vcodec copy -ac 1 "${i%.mp4}-fixed.mp4"
    fi
done

david-christiansen

#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"))

david-christiansen

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))

david-christiansen

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

david-christiansen

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 [

david-christiansen

data Typ =
    IntTyp
  | BolTyp
  | FunTyp Typ Typ

toType : Typ -> Type
toType IntTyp       = Integer
toType BolTyp       = Bool
toType (FunTyp x y) = toType x -> toType y

david-christiansen

module NotElem

import Language.Reflection.Elab
import Language.Reflection.Utils

import Data.List


emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible

david-christiansen

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

david-christiansen

||| Binary parsing, based on the stuff in Power of Pi
module Bin


import System

import Data.So
import Data.Vect
import Bytes

david-christiansen

module ClassNonsense

import Language.Reflection.Elab

class Foo t where
  constructor MkFoo
  foo : t

myFoo : Foo Nat
myFoo = MkFoo 1