gallais

module With where

open import Data.Nat using (ℕ ; _+_)
open import Relation.Binary.PropositionalEquality

module UsingWith where
  
  plus-n-0 : (n : ℕ) → n + 0 ≡ n
  plus-n-0 ℕ.zero    = refl
  plus-n-0 (ℕ.suc n) with n + 0 | plus-n-0 n

gallais

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

module Tails where

import Data.Function

newtype Mu f = In { out :: f (Mu f) }


fold :: Functor f => (f a -> a) -> Mu f -> a

gallais

Inductive term : Set :=
| true : term
| false : term
| ifthenelse : term -> term -> term -> term.

Inductive step : term -> term -> Prop :=
  | iota1 : forall l r, step (ifthenelse true l r) l
  | iota2 : forall l r, step (ifthenelse false l r) r
  | econ1 : forall b c l r, step b c -> step (ifthenelse b l r) (ifthenelse c l r)
  | econ2 : forall b l m r, step l m -> step (ifthenelse b l r) (ifthenelse b m r)

gallais

open List

type 'a tree = Node of 'a * 'a tree * 'a tree | Null

type 'a init_last = 'a list * 'a list

let to_list (xs : 'a init_last) : 'a list =
  let (init, last) = xs in init @ rev last

let push_top (a : 'a) (xs : 'a init_last) : 'a init_last =

gallais

Inductive perm (A:Set): (list A) -> (list A) -> Prop:=
 p_refl: forall l:(list A), perm A l l
|p_trans: forall l m n: (list A), (perm A l m) -> (perm A m n) -> perm A l n
|p_ccons: forall (a b: A) (l:(list A)), 
	perm A (cons a (cons b l)) (cons b (cons a l))
|p_cons: forall (a:A) (l m: (list A)), (perm A l m) -> perm A (cons a l) (cons a m).

Fixpoint swap (A:Set) (l:(list A)) {struct l}: (list A) :=
    match l with 
      nil  => nil

gallais

type z = Z
type +'a s = S

type _ nat =
  | Z : ('l * 'l) nat
  | S : ('l * 'm) nat -> ('l * 'm s) nat

let rec add : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1

gallais

module Even where

open import Data.Bool
open import Data.Nat
open import Function

open import Relation.Binary.PropositionalEquality

even : ℕ → Bool
even 0             = true

gallais

{-# LANGUAGE ScopedTypeVariables #-}

module UnfoldTree where

data Tree v e  = Node v [(e,Tree v e)]

unfold :: forall s v e. (s -> (v, [(e,s)])) -> s -> Tree v e
unfold next seed = uncurry Node $ fmap rec $ next seed where

  rec :: [(e,s)] -> [(e, Tree v e)]

gallais

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

module UnitLength where

newtype Length (a::UnitLength) b = Length { payload :: b } deriving (Eq,Show)
data UnitLength = Meter
                | KiloMeter
                | Miles

gallais

module LambdaLifting where

open import Level using (Level)

module Identity (A : Set) where

  identity : A → A
  identity = λ x → x

data _∈_ {ℓ : Level} {A : Set ℓ} (a : A) : (B : Set ℓ) → Set where