gallais

(*
Fixpoint boringFail (m : nat) : True :=
  match m with
   | S (S m) => boringFail (S m)
   | _       => I
  end.
*)

Fixpoint boringWork (m : nat) : True :=
  match m with

gallais

import Data.Maybe
import Control.Monad
import Control.Applicative
import Graphics.Gloss
import Graphics.Gloss.Interface.Pure.Game

type Coordinates = (Int, Int)

data Player = Nought | Cross

gallais

{-# LANGUAGE GADTs #-}

module NthElement where

import Data.Functor
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.State

data Tree a where

gallais

open import Level
import Data.AVL.Sets
open import Data.String as String
open import Relation.Binary using (module StrictTotalOrder)

open import Data.Product
open import Function
open import Relation.Binary

gallais

module LEM where

open import Data.Empty
open import Data.Product
open import Function
open import Relation.Nullary

∄⇒∀ : {A : Set} {B : A → Set} →
      ¬ (∃ λ a → B a) →
      ∀ a → ¬ (B a)

gallais

Require Import Arith.
Require Import List.
Local Open Scope list_scope.

Inductive SubListsRel (n : nat) : forall (ns : list nat)
                      (mss : list (list nat)), Prop :=

  | base      : SubListsRel n nil (nil :: nil)

  | consEq    : forall ns m mss,

gallais

Require Import Equations.

Inductive Fin : nat -> Type :=
  | fz {n : nat} : Fin (S n)
  | fs {n : nat} : Fin n -> Fin (S n).

Lemma FinO_elim : Fin O -> False.
Proof.
inversion 1.
Qed.

gallais

module Datatype where

open import Data.Empty hiding (⊥-elim)
open import Data.Nat
open import Data.Bool
open import Data.List
open import Relation.Nullary

¬n<0 : {n : ℕ} → ¬ (n < 0)
¬n<0 ()

gallais

Require Import Reals.

Open Scope R_scope.

Goal forall x, x <> 0 -> 1 / x <> 0.
intros.
 unfold Rdiv; rewrite Rmult_1_l.
 apply Rinv_neq_0_compat.
 assumption.
Qed.

gallais

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

module Vec where