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

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

(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

package dep

import scala.language._

object Dep extends App {

  sealed trait Nat {
    type Plus[M <: Nat] <: Nat
    def plus[M <: Nat](m: M): Plus[M]
  }

david-christiansen

Keybase proof

I hereby claim:

• I am david-christiansen on github.
• I am d_christiansen (https://keybase.io/d_christiansen) on keybase.
• I have a public key whose fingerprint is 2709 89EB 2214 50FA DD57 54A8 34B5 BFDB 0942 94C3

To claim this, I am signing this object:

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

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

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

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

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