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

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

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

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

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

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 Main

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

%default covering
%access public export

paren : String -> String

joom

module Table where
import Data.List

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

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

||| Hacky and rudimentary hint database for Idris using elaborator reflection.
||| You can now write tactics that does `getHints`
||| and try to prove the goal with the lemmas there.
module Hints
import Language.Reflection.Utils
%language ElabReflection
%access public export

||| The hint to pass the machine generated names. Note that the word hint here
||| is used literally, not in the theorem prover sense.