david-christiansen

module HList

%default total

data HList : List Type -> Type where
  (::) : t -> (xs : HList ts) -> HList (t :: ts)
  Nil : HList []

foo : HList [Int, String, Int]
foo = [3, "yes", 17]

david-christiansen

module PropDemo

data GreaterThanTwo : Nat -> Type where
  threeOK : GreaterThanTwo 3
  moreOK : GreaterThanTwo n -> GreaterThanTwo (S n)

total sumGreater : GreaterThanTwo n -> GreaterThanTwo m -> GreaterThanTwo (n + m)
sumGreater threeOK mOK = moreOK (moreOK (moreOK mOK))
sumGreater (moreOK nOK') mOK = moreOK (sumGreater nOK' mOK)

david-christiansen

module Lambda

%default total

infixr 8 ==>

data T : Type where
  U : T
  NAT : T
  (*) : T -> T -> T

david-christiansen

module Addition


class Plus (n : Nat) (m : Nat) (o : Nat) where {}

instance Plus Z m m where {}

instance Plus n m o => Plus (S n) m (S o) where {}

parameters (n : Nat, m : Nat)

david-christiansen

module Bugfind



import Language.Reflection
import Language.Reflection.Util

foo : TT
foo = Erased

david-christiansen

drc@drc:~/Documents/Code/Idris/error-reflection-test$ idris ErrorTest.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.10.1-git:5361547
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ./ErrorTest.idr
*ErrorTest> the Nat ""
ERROR HAPPENED!

david-christiansen

import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

total
cadr :  (xs : List a)
     -> {auto cons1 : isCons xs = True}
     -> {auto cons2 : isCons (tail xs cons1) = True}
     -> a

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 PlusRewrite

import Language.Reflection
import Language.Reflection.Utils

rewrite_plusSuccRightSucc : TT -> Maybe Tactic
rewrite_plusSuccRightSucc `(plus ~n (S ~m)) = Just $ Rewrite `(plusSuccRightSucc ~n ~m)
rewrite_plusSuccRightSucc `(S ~n) = rewrite_plusSuccRightSucc n
rewrite_plusSuccRightSucc `(plus ~n ~m) = rewrite_plusSuccRightSucc n <|> rewrite_plusSuccRightSucc m
rewrite_plusSuccRightSucc _ = Nothing

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