ggreif

*.agdai
agda-stdlib-*

ggreif

module Set where

import Data.List (nub)
--import qualified Data.List.NonEmpty as NE
--import Bag

-- a set is a functor with a splitter

class Applicative f => Set f where
  split :: f a -> (f a, f a) -- non-deterministic (instance-defined) monotonic splitter

ggreif

import Prelude

-- * Power series
--
-- treat power series representations of functions
-- like numbers and derivatives

-- ** Background
--
-- http://www.cs.dartmouth.edu/~doug/powser.html

ggreif

-- * Stuff

{-# LANGUAGE DataKinds, RankNTypes, NoMonomorphismRestriction, GADTs, StandaloneDeriving, ScopedTypeVariables #-}

module Nameless where

import Prelude hiding (abs)

-- * Pictures

ggreif

 {-# LANGUAGE FlexibleInstances, RankNTypes #-}

module Hutton where

import Test.QuickCheck

-- Hutton's razor
--
data Expr = Val Integer
          | Expr `Add` Expr

ggreif

import Data.Char

ch = chr . (+65)

-- east quadrant
ulam x y | x > y && x > -y   = (x*2 - 1)^2 + (x + y) - 1

-- north quadrant
ulam x y | x <= y && x > -y  = (y*2)^2 - (x + y)