gallais

module Sorting where

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary

gallais

\documentclass{article}
%include lhs2TeX.fmt
%include lhs2TeX.sty
%include polycode.fmt
\begin{document}

\begin{code}
module Equal where

data _≡_ {a} {A : Set a} (x : A) : A → Set a where

gallais

Require Import Complex Cpow Ctacfield.

Require Import Nsatz.


Lemma Csth : Setoid_Theory C (@eq C).
constructor;red;intros;subst;trivial.
Qed.

Instance Cops: (@Ring_ops C C0 C1 Cadd Cmult Cminus Copp (@eq C)).

gallais

module Disjunctive where

open import Data.Product
import Data.Bool as 𝔹
open import Data.Bool.Properties
open import Data.Nat
open import Data.Fin
open import Data.Vec hiding ([_])

open import Algebra.Structures

gallais

module lte10 where

open import Data.Empty
open import Data.Unit
open import Data.Nat as ℕ
open import Data.Maybe
open import Data.Vec

open import Function

gallais

{-# LANGUAGE GADTs#-}

data Lam a  where
  Var :: a -> Lam a
  App :: Lam a -> Lam a -> Lam a
  Lam :: Lam (Maybe a) -> Lam a

mapLam :: (a -> b) -> Lam a -> Lam b
mapLam f (Var a)   = Var $ f a
mapLam f (App t u) = mapLam f t `App` mapLam f u

gallais

Require Import NArith.

Fixpoint sum_of (f : nat -> nat) (n : nat) : nat :=
match n with
  | O   => f O
  | S m => f (S m) + sum_of f m
end.

Lemma sum_of_pow : forall n,
 S (sum_of (NPeano.pow 2) n) = NPeano.pow 2 (S n).

gallais

module Main where

data Trie a =
    Leaf
  | Node (Trie a) a (Trie a)

data Code   = Dot | Dash
type Word   = [ Code ]
type Phrase = [ Word ]
type Dict   = Trie (Maybe Char)

gallais

module Categories.Fam where

open import Level
import Function as Fun
open import Data.Product
open import Relation.Binary

open import Categories.Category
open import Categories.Support.EqReasoning
open import Categories.Support.PropositionalEquality

gallais

{-# LANGUAGE DeriveDataTypeable #-}

module LEM where

import Control.Exception
import Data.Typeable
import System.IO.Unsafe

data Void