gallais

Inductive fin : nat -> Set :=
| F1 : forall {n : nat}, fin (S n)
| FS : forall {n : nat}, fin n -> fin (S n).

Definition C {m : nat} (x : fin (S m)) :=
  { x' | x = FS x' } + { x = F1 }.

Definition case {m : nat} (x : fin (S m)) : C x :=
match x in fin (S n) return { x' | x = FS x' } + { x = F1 } with
  | F1    => inright eq_refl

gallais

Require Import PeanoNat.
Require Import List.
Import ListNotations.


Fixpoint iota (n : nat) : list nat :=
  match n with
    | 0   => []
    | S k => iota k ++ [k]
  end.

gallais

open import Data.String


record Print (A : Set) : Set where
  field
    print : A → String
open Print {{…}} public

mutual
  data α : Set where

gallais

module NbeIsASemantics where

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Agda.Builtin.List

data Ty : Set where
  α   : Ty
  _⇒_ : Ty → Ty → Ty

gallais

{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall              #-}

module AllHList where

gallais

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

module Terminal where

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

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

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

module ICofree where

data Nat = Z | S Nat

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)