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

module CanonicalStructures where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

open import Function

gallais

module PrintNumber where

pad :: Char -> [String] -> [String]
pad c xs = ys where
  (ys, n)         = foldr cons ([],0) xs
  cons x (acc, m) = ((replicate (n - m') c ++ x) : acc, max m m')
    where m' = length x

gallais

module NP where

open import Level as L using (Level)
open import Data.Nat
open import Data.List
open import Data.String as String hiding (show)
open import Function

data NP {ℓ ℓ′ : Level} (f : Set ℓ → Set ℓ′) :
        (xs : List (Set ℓ)) → Set (L.suc ℓ L.⊔ ℓ′) where

gallais

module InstanceLoop where

record Target (A : Set) : Set where
  constructor mkTarget
  field
    a : A

instance

  loop : {A : Set} {{tA : Target A}} → Target A

gallais

Require Import Equations.
Require Import List.
Require String. Open Scope string_scope.

Ltac Case str :=
  let val := eval compute in (String.append "case " str)
  in idtac val.

Equations append {A : Type} (xs ys : list A) : list A
:= append A []          ys := ys

gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

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

gallais

module Data.Cellular where

import Data.Monoid
import Data.Function.Memoize

newtype Cellular g a = Cellular { delta :: (g -> a) -> a }

step :: Monoid g => Cellular g a -> (g -> a) -> (g -> a)
step (Cellular d) init g = d (init . (g <>))

gallais

module ConcatVec where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Vec
open import Function
open import Relation.Binary.PropositionalEquality

data Plus (m : ℕ) : (n p : ℕ) → Set where
  base : Plus m 0 m

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