View Test.idr
module Test | |
import Provider | |
import Database | |
import Queries | |
%language TypeProviders | |
%link C "sqlite3api.o" |
View New proof automation
%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 |
View SExpParse.idr
module SExpParse | |
import Lightyear.Core | |
import Lightyear.Combinators | |
import Lightyear.Strings | |
%default total | |
data MessageFmt = KWD String | |
| STRING |
View Test.idr
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 |
View Prov.idr
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 |
View Output
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 |
View FizzBuzz.idr
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 |
View gist:a463bdb0086dab60c72b
(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)) "...") |
View gist:2ba5e03910666ae27203
;;; 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 |
View Snoc.idr
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 |
OlderNewer