timjb

module SortedList

-- Based on http://mazzo.li/posts/AgdaSort.html

import Decidable.Decidable
import Decidable.Order
import Uninhabited

%default total

timjb

{-# LANGUAGE NoMonomorphismRestriction #-}

-- http://www.cut-the-knot.org/Curriculum/Geometry/Tromino.shtml

module Trominoes where

import Diagrams.Prelude
import Diagrams.Backend.SVG
import Diagrams.Backend.SVG.CmdLine

timjb

Kartoffel-Maronen-Suppe

Zutaten

• 400g Maronen
• 1 Zwiebel
• 2 Knoblauchzehen
• 4-5 Kartoffeln
• 1/2l Brühe
• 200g Sahne

timjb

-- Vorlesung "Homologische Algebra", Übungsblatt 1, Aufgabe 2

module CosimplicialIdentities where

open import Function
open import Data.Product
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat hiding (_≤_; _<_; compare) renaming (suc to s)
open import Data.Nat.Properties hiding (strictTotalOrder)
open import Data.Fin hiding (compare)

timjb

Idris> :load test.idr 
*test> xAssoc (MkX (3 + 4)) (MkX 5)
MkX 12 : X 12
*test> xAssoc' (MkX (3 + 4)) (MkX 5)
replace (sym (plusAssociative' 3 4 5))
        xPlus
        (MkX 7)
        (MkX 5) : X 12
*test> xAssoc'' (MkX (3 + 4)) (MkX 5)
MkX 12 : X 12

timjb

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE LiberalTypeSynonyms #-}

timjb

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}

module WithFunctor where

newtype (:.:) f g a = Comp { getComp :: f (g a) } deriving (Show, Eq)

instance (Functor f, Functor g) => Functor (f :.: g) where
  fmap f = Comp . fmap (fmap f) . getComp

timjb

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}

module BoundedExistentials where

import GHC.Exts (Constraint)

class Constraint1 c where
  type Constr1 c a :: Constraint

timjb

module Data.LazyList

%default total
%access public

data LazyListCell a = Nil | (::) a (Lazy (LazyListCell a))

LazyList : Type -> Type
LazyList a = Lazy (LazyListCell a)

timjb

module Data.RealTimeQueue

-- adapted from Chris Okasaki's `Purely Functional Data Structures`, figure 7.1

%default total

data LazyVectCell : Nat -> Type -> Type where
  Nil  : LazyVectCell Z a
  (::) : (x : a) -> (xs : Lazy (LazyVectCell n a)) -> LazyVectCell (S n) a