david-christiansen

  %reflection
  solveHasTable : Type -> Tactic
  solveHasTable (HasTable (_::tl) name s) =
    Try (Refine "Here" `Seq` Solve)
        (Refine "There" `Seq` (Solve `Seq` solveHasTable (HasTable tl name s)))
  solveHasTable (HasTable (a++b) _ _) = Refine "Here" `Seq` Solve
  solveHasTable (HasTable _ name s) = Refine "Here" `Seq` Solve

david-christiansen

module Test

import Provider

import Database
import Queries

%language TypeProviders

%link C "sqlite3api.o"

david-christiansen

module SExpParse

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%default total

data MessageFmt = KWD String
                | STRING

david-christiansen

module Main

import System.Random.TF.Gen

genNums : Int -> TFGen -> IO TFGen
genNums i gen = if i > 0 then
                   let (n, gen') = tfGenNext gen in
                   do putStrLn (show i ++"\t0x"++show n)
                      genNums (i-1) (fst (split gen'))
                else return gen

david-christiansen

import QuickCheck

import Providers

%language TypeProviders

prop_RevRev : Eq a => List a -> Bool
prop_RevRev xs = reverse (reverse xs) == xs

stupid : List a -> List a

david-christiansen

drc@drc:~/tmp$ idris Quasiquote.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.13.1-git:f8ec244
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./Quasiquote.idr

david-christiansen

module FizzBuzz

-- Dependently-typed FizzBuzz, about 5 years late to the party.

-- A specification of the problem.  Each constructor tells the conditions
-- under which it can be applied, and the "auto" keyword means that proof
-- search will be used in the context where they are applied to fill them
-- out. For instance, applying `N` to some Nat fails unless there's a proof in
-- scope that the argument meets the criteria.
data FB : Nat -> Type where

david-christiansen

(defun helm-ghc-errors-in-buffer ()
  (with-current-buffer helm-current-buffer
    (remove-if-not #'(lambda (o) (overlay-get o 'ghc-check))
                   (overlays-in (point-min) (point-max)))))

(defun helm-ghc-describe-overlay (o)
  (cl-flet ((abbreviate (str)
                        (if (> (length str) fill-column)
                            (concat (substring str 0 (- fill-column 3)) "...")

david-christiansen

;;; Helm support for finding my stuff
(defvar helm-david-christiansen-git-repo-list nil
  "The Git repos found for my Helm launcher.")
(defvar helm-david-christiansen-git-repo-finder-process nil
  "The process finding Git repos for my Helm launcher.")
(defun helm-david-christiansen-git-repo-finder-output-filter (proc string)
  (when (buffer-live-p (process-buffer proc))
    (with-current-buffer (process-buffer proc)
      (let ((moving (= (point) (process-mark proc))))
        (save-excursion

david-christiansen

module Snoc

data SnocList : List a -> Type where
  SnocNil : SnocList []
  Snoc : (xs : List a) -> (x : a) -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs
snocList [] = SnocNil
snocList (x :: xs) with (snocList xs)
  snocList (x :: []) | SnocNil = Snoc [] x