{{ message }}

Instantly share code, notes, and snippets.

🐈
=^_^=

# Dan Fruminco-dan

🐈
=^_^=
• Nijmegen
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
Last active Aug 29, 2015
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 ()
Created Jan 16, 2015
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 :=
Created Jan 16, 2015
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.
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
Created Oct 26, 2012
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 => \⌣
Created Nov 16, 2012
View gist:4088395
 (* Kevin Sullivan , 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
Created Dec 13, 2012