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 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

gallais

{-# OPTIONS --no-termination-check --no-positivity-check #-}

module MutuallyDefined where

open import Data.Nat as ℕ
open import Data.Fin 
open import Function

data Tie {n : ℕ} (F : (Fin n → Set) → Fin n → Set) (k : Fin n) : Set where
  ⟨_⟩ : (v : F (Tie F) k) → Tie F k

gallais

{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE RankNTypes          #-}

module MutuallyDefinedList where

gallais

Inductive Vector (A : Type) : nat -> Type :=
  | nil  : Vector A O
  | cons : forall n, A -> Vector A n -> Vector A (S n).

Definition head (A : Type) (n : nat) (v : Vector A (S n)) : A.
refine (
  (match v in Vector _ m return m = S n -> A with
   | nil          => _
   | cons _ hd tl => fun _ => hd
  end) (eq_refl (S n))).