gallais

open import Data.Nat

module atleastn (n : ℕ) {a} (A : Set a) where

open import Data.List using (List; length)
open import Data.Vec

record SizedList : Set a where
  field list : List A
        size : length list ≥ n

gallais

open import Data.String.Base
open import Data.Nat.Base
open import Data.List.Base
open import Relation.Binary.PropositionalEquality

infix 5 _at_
record Variable : Set where
  constructor _at_
  field name   : String

gallais

Inductive T :=
  | Var : nat -> T
  | App : T -> T -> T.

Inductive S e : Prop := 
| def: forall R, (forall i, R i -> S i) ->
       (forall e', R e' -> S (App e e')) -> S e.

Definition def' :
  forall e, (forall e', S e' -> S (App e e')) -> S e.

gallais

Require Import ZArith.

Local Open Scope Z_scope.

Section FF.

Parameter A : Type.
Parameter (a b c d : A).

Definition FF := Z -> Z -> A.

gallais

module Instrumented where

import Control.Monad.State

data Counters = Counters
  { swaps       :: !Int
  , comparisons :: !Int
  }

type Instrumented = State Counters

gallais

{-# LANGUAGE DeriveFunctor #-}

module MonadTree where

import Control.Monad
import Control.Monad.Fix

newtype Tree m a = Tree { runTree :: m (Node m a) }
  deriving (Functor)

gallais

{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}

module ICofree where

data Nat = Z | S Nat

gallais

module Main where

import Codec.Picture

intersection :: Image PixelRGBA8 -> Image PixelRGBA8 -> Int -> Int -> PixelRGBA8
intersection a b x y =
  let (PixelRGBA8 a1 a2 a3 a4) = pixelAt a x y
      (PixelRGBA8 b1 b2 b3 b4) = pixelAt b x y
      as = [a1, a2, a3]
      bs = [b1, b2, b3]

gallais

type comparison = LT | EQ | GT

module type ORDERED =
sig
  type t
  val compare : t -> t -> comparison
end

module type SORTEDLIST =
  functor (O : ORDERED) ->

gallais

{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE Rank2Types                 #-}

module Terminal where