View VeryFun.idr
module VeryFun | |
class VeryFun (f : Type -> Type) (dict : Functor f) | f where | |
funIdentity : {a : Type} -> (x : f a) -> | |
map @{dict} id x = id x | |
funComposition : {a : Type} -> {b : Type} -> | |
(x : f a) -> (g1 : a -> b) -> (g2 : b -> c) -> | |
map @{dict} (g2 . g1) x = (map @{dict} g2 . map @{dict} g1) x | |
instance VeryFun List %instance where |
View MkMonoid.idr
module MkMonoid | |
import Language.Reflection.Elab | |
||| Generate a Monoid dictionary | |
total | |
mkMonoid : Semigroup a => (neutral : a) -> Monoid a | |
mkMonoid @{semigroup} neutral = mkMonoid' _ semigroup neutral | |
where | |
mkMonoid' : (a : Type) -> (constr : Semigroup a) -> a -> Monoid a |
View MkShow.idr
module MkShow | |
import Language.Reflection.Elab | |
mkShow : (a : Type) -> (a -> String) -> Show a | |
mkShow = %runElab (fill (Var (SN (InstanceCtorN `{Show}))) *> solve) | |
shower : Show Float | |
shower = mkShow _ (const "oops") |
View fix-audio.sh
#!/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 |
View PlusRewrite.idr
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 |
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 FunErrTest.idr
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 |
View gist:8336956
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! |
View Bugfind.idr
module Bugfind | |
import Language.Reflection | |
import Language.Reflection.Util | |
foo : TT | |
foo = Erased |