Skip to content

Instantly share code, notes, and snippets.

🦊
^_^

Dan Frumin co-dan

🦊
^_^
  • Nijmegen
Block or report user

Report or block co-dan

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@co-dan
co-dan / SeqFoldable.hs
Created Apr 7, 2014
Sequence-algebras
View SeqFoldable.hs
{-# 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
View Home.hs
{-# 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 ()
View induction.v
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 :=
View nat_well_founded.v
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
co-dan / Dice.hs
Created Feb 22, 2015
A simple dice rolling bot based on `pipes-irc'. Responds to commands like "roll d20+d4+3"
View Dice.hs
{-# 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
View smile.pl
#!/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 => \&smile;
View gist:4088395
(* 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
co-dan / MaybeT.hs
Created Dec 13, 2012
Maybe monad transformer
View MaybeT.hs
{-# 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
co-dan / gist:4358385
Created Dec 22, 2012
Generating HTML page from Calibre's catalog
View gist:4358385
{-# 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
View Tests.lhs
> 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) (
You can’t perform that action at this time.