This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
||| Red-black trees that intrinsically verifies it preserves the color invariants. | |
||| Originally written by Dan Licata in Agda. | |
module RedBlack | |
%default total | |
%hide Prelude.List.toList | |
data Color = Red | Black | |
mutual | |
||| Idris has induction-recursion but not induction-induction |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Table where | |
import Data.List | |
t1 :: [[String]] | |
t1 = [ ["name", "age"] | |
, ["Obama", "56"] | |
, ["Elizabeth", "91"] | |
, ["Josiah Edward \"Jed\" Bartlet", "76"] | |
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
import Control.Monad.State | |
import Data.SortedMap | |
import Data.SortedSet | |
%default covering | |
%access public export | |
paren : String -> String |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let val plus = \(n:nat) \(m:nat) rec m { | |
z => n | |
| s(x) with y => s(y) | |
} | |
in let val pred = \(n : nat) rec n { | |
z => z | |
| s(x) with y => x | |
} | |
in let val minus = \(n:nat) \(m:nat) rec m { | |
z => n |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module SimplyTypedLambdaCalculus where | |
open import Data.Bool | |
open import Data.Nat hiding (erase) | |
import Data.Unit | |
open import Data.Maybe | |
open import Data.Product | |
open import Data.Sum | |
open import Relation.Binary.PropositionalEquality hiding ([_]) | |
open import Relation.Nullary |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Parsing the API result from wesleyan/spec | |
{-# LANGUAGE DeriveGeneric #-} | |
module Event where | |
import Control.Monad (mzero) | |
import Control.Applicative | |
import Data.Aeson | |
import GHC.Generics |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.List (partition) | |
import Control.Arrow ((***)) | |
idValidate n = (length ds == 11) && check1 && check2 | |
where ds = map (\x -> read [x] :: Int) (show n) | |
(o, e) = map snd *** map snd $ partition (\(x,_)->odd x) $ zip [1..9] ds | |
check1 = ds !! 9 == (sum o * 7 - sum e) `mod` 10 | |
check2 = ds !! 10 == sum (init ds) `mod` 10 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import System.Random | |
data Move = Rock | Paper | Scissors deriving (Show, Eq, Enum) | |
instance Ord Move where | |
(<=) x y = x == y || (x,y) `elem` [(Rock,Paper),(Paper,Scissors),(Scissors,Rock)] | |
humanSelect :: IO Move | |
humanSelect = fmap (toEnum . read) getLine |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
% adds X to the beginning of each list in the second argument. | |
% Haskell equiv: map (X:) secondArg | |
cons_all(_, [], []). | |
cons_all(X, [H|Tl], [[X|H]|NewTl]) :- | |
cons_all(X, Tl, NewTl). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; My packages installed: evil, evil-leader, undo-tree, evil-surround (not in MELPA), color-theme-wombat, haskell-mode. | |
;; packages | |
(setq package-archives '(("gnu" . "http://elpa.gnu.org/packages/") | |
("org" . "http://orgmode.org/elpa/") | |
("marmalade" . "http://marmalade-repo.org/packages/") | |
("melpa-stable" . "http://melpa-stable.milkbox.net/packages/"))) | |
(add-to-list 'load-path "~/.emacs.d") | |
(package-initialize) | |
(evil-mode 1) |