co-dan

#!/usr/bin/perl

use Irssi;
use vars qw($VERSION %IRSSI);
use warnings;
use strict;
##use common::sense;
##use Modern::Perl 2012;
Irssi::command_bind smile => \⌣

co-dan

(* Kevin Sullivan <[email protected]>, writing to the Coq-Club: *)
(* My students presented two solutions to the simple problem of applying a *)
(* function f n times to an argument x (iterated composition). The first says *)
(* apply f to the result of applying f n-1 times to x; the second,  apply f n-1 *)
(* times to the result of applying f to x. I challenged one student to prove that *)
(* the programs are equivalent. This ought to be pretty easy based on the *)
(* associativity of composition. Your best solution? *)

Fixpoint ant {X: Type} (f: X->X) (x: X) (n: nat) : X :=
match n with

co-dan

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
module MaybeT where
-- Maybe monad transformer
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State

newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }

co-dan

{-# LANGUAGE OverloadedStrings, ScopedTypeVariables #-}
module Main where

import Text.Blaze.Html5
import qualified Text.Blaze.Html5 as H
import Text.Blaze.Html5.Attributes
import qualified Text.Blaze.Html5.Attributes as A
import Text.Blaze.Html.Renderer.Pretty

import Data.Csv

co-dan

> showReadIso :: Expr -> Bool
> showReadIso e = parseExpr (show' e) == e


*Tests> quickCheck showReadIso
*** Failed! Falsifiable (after 34 tests): 
Prod (Variable "d") (Prod (Variable "b") (Universe 9) (Prod (Variable "a") (Prod (Variable "c") (Var (Variable "a")) (App (Lambda (Variable "c") (Var (Variable "b")) (Universe 8)) (Prod (Variable "a") (Universe 1) (Var (Variable "c"))))) (Prod (Variable "b") (Lambda (Variable "c") (App (Universe 2) (Universe 5)) (Var (Variable "c"))) (App (Var (Variable "b")) (Lambda (Variable "d") (Var (Variable "a")) (Universe 7)))))) (App (Prod (Variable "a") (Lambda (Variable "d") (Universe 9) (Prod (Variable "a") (App (Var (Variable "b")) (Var (Variable "d"))) (App (Var (Variable "a")) (Var (Variable "a"))))) (Prod (Variable "a") (App (Prod (Variable "c") (Var (Variable "b")) (Var (Variable "c"))) (Prod (Variable "d") (Var (Variable "b")) (Universe 10))) (Prod (Variable "d") (Lambda (Variable "a") (Var (Variable "c")) (Var (Variable "d"))) (Prod (Variable "c") (Universe 5) (

co-dan

{-# LANGUAGE OverloadedStrings, DeriveDataTypeable, ScopedTypeVariables #-}

import Database.PostgreSQL.Simple
import Database.PostgreSQL.Simple.FromRow
import Database.PostgreSQL.Simple.FromField

import Data.Typeable

import Control.Applicative

co-dan

module Automata where

import Prelude hiding (or, foldl)
import Control.Monad
import Data.Foldable hiding (elem)
import Control.Monad.Identity


data Automata q s m = A { states :: [q]
                        , trans :: (q, s) -> m q

co-dan

import Data.Functor.Compose

data N n = N { unN :: n Int }
f :: (Functor n, Functor m) => (Int -> m Int) -> N n -> N (Compose n m) 
f h = N . Compose . fmap h . unN
-- f h (N x) = N $ Compose (fmap h x)

co-dan

import Text.XML.HXT.Core

doc = "/Users/dan/Downloads/greader-takeout/Reader/subscriptions.xml"

type Subscriptions = [(String, String)]

getSites :: ArrowXml a => a XmlTree (String,String)
getSites =   isElem 
         >>> hasAttrValue "type" (=="rss") 
         >>> getAttrValue "htmlUrl" &&& getAttrValue "xmlUrl"

co-dan

(setq load-path (append '("~/projects/emacs/org-mode/lisp" "~/projects/emacs/org-mode/contrib/lisp") load-path))

(require 'org)
(custom-set-faces
 '(org-link ((t (:foreground "aqua" :underline t))))
 '(org-date ((t (:foreground "RoyalBlue1" :underline t)))))

;; IDO
(setq org-completion-use-ido t)