gallais

module Joomy where

open import Level using (Level)

open import Data.List.Base
  as List
  using ()
  renaming (List to [>_]; [] to [>]; _∷_ to _:>_)

open import Data.Nat.Base using (ℕ; _+_; _≤_)

gallais

Require Import Coq.Setoids.Setoid.
Require Import Arith.

Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).

Definition times2 : forall n, n + n = 2 * n := fun n =>
  `Begin

gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

gallais

(*
   We don't really care about the data constructors here
   but they are needed, cf:
   https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00190.html
 *)
type zero    = Zero
type 'a succ = Succ

(*
   []   has length 0

gallais

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Deriving where

import Data.Kind (Type)

newtype Cst a   i = MkCst { runCst :: a }
newtype Idt     i = MkIdt { runIdt :: i }
newtype Prd k l i = MkPrd { runPrd :: (k i, l i) }

gallais

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Control.Concurrent (forkIO, MVar, newEmptyMVar, putMVar, takeMVar)

import Data.Kind (Type)

gallais

module ShaSearch where

import System.Process (readProcess)

-----------------------------------------------
-- Using the list monad to generate all the
-- hexadecimal words of a given length

-- All the hexadecimal characters
hexa :: [Char]

gallais

module Currying where

open import Level
open import Data.Product as P using (_×_ ; _,_)
open import Function

data Universe (ℓ : Level) : Set (suc ℓ) where
  set  : (A : Set ℓ) → Universe ℓ
  _**_ : (u₁ u₂ : Universe ℓ) → Universe ℓ

gallais

{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE PolyKinds                 #-}

module ImperativeDSL where

gallais

Inductive T :=
  | Var : nat -> T
  | App : T -> T -> T.

Inductive S e : Prop := 
| def: forall R, (forall i, R i -> S i) ->
       (forall e', R e' -> S (App e e')) -> S e.

Definition def' :
  forall e, (forall e', S e' -> S (App e e')) -> S e.