co-dan

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module SeqFoldable where

import           Prelude hiding (drop, take)

import           Data.Functor.Foldable
import           Data.Sequence         (Seq, ViewL (..), (<|))
import qualified Data.Sequence         as S

co-dan

{-# LANGUAGE OverloadedStrings #-}

module Controllers.Home (homeRoutes) where

import Web.Scotty
import Data.Monoid                              (mconcat)
import qualified Database.RethinkDB as R
import qualified Database.RethinkDB.NoClash

homeRoutes :: ScottyM ()

co-dan

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
         (f0 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (3+m) (g_plus3 m e)) 
         (f1 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (5+m) (g_plus5 m e)) 
         (n : nat) (e: gorgeous n) : P n e :=

co-dan

Require Import Rel.
Require Import Coq.Init.Wf.

Theorem nat_wo: well_founded lt.
Proof.
  intro n.
  assert (forall y x, x < y -> Acc lt x) as A.
  induction y.
  + intros x H; inversion H.
  + intros x H'. apply Acc_intro.

co-dan

{-# LANGUAGE OverloadedStrings #-}
import           Control.Monad
import           Control.Monad.Identity
import           Control.Monad.Random
import qualified Data.ByteString                        as BS
import qualified Data.ByteString.Char8                  as B
import           Data.Maybe
import           Data.Set                               as S
import           Data.Traversable                       as T
import           Pipes

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 <sullivan.kevinj@gmail.com>, 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) (