joom

||| 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

joom

module Table where
import Data.List

t1 :: [[String]]
t1 = [ ["name", "age"]
     , ["Obama", "56"]
     , ["Elizabeth", "91"]
     , ["Josiah Edward \"Jed\" Bartlet", "76"]
     ]

joom

module Main

import Control.Monad.State
import Data.SortedMap
import Data.SortedSet

%default covering
%access public export

paren : String -> String

joom

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

joom

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

joom

-- 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

joom

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

joom

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

joom

% 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).

joom

;; 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)