gallais

{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall              #-}

module AllHList where

gallais

module NbeIsASemantics where

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Agda.Builtin.List

data Ty : Set where
  α   : Ty
  _⇒_ : Ty → Ty → Ty

gallais

open import Data.String


record Print (A : Set) : Set where
  field
    print : A → String
open Print {{…}} public

mutual
  data α : Set where

gallais

Require Import PeanoNat.
Require Import List.
Import ListNotations.


Fixpoint iota (n : nat) : list nat :=
  match n with
    | 0   => []
    | S k => iota k ++ [k]
  end.

gallais

Inductive fin : nat -> Set :=
| F1 : forall {n : nat}, fin (S n)
| FS : forall {n : nat}, fin n -> fin (S n).

Definition C {m : nat} (x : fin (S m)) :=
  { x' | x = FS x' } + { x = F1 }.

Definition case {m : nat} (x : fin (S m)) : C x :=
match x in fin (S n) return { x' | x = FS x' } + { x = F1 } with
  | F1    => inright eq_refl

gallais

module poc.FiniteMap where

open import Function
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

record _↔_ (A B : Set) : Set where
  field push : A → B
        pull : B → A

gallais

module Accessibility where

data Acc {A : Set} (R : A → A → Set) (a : A) : Set where
  step : (∀ b → R b a → Acc R b) → Acc R a 

□^ : ∀ {A : Set} (R : A → A → Set) → (A → Set) → (A → Set)
□^ R P a = ∀ b → R b a → P b

[_] : {A : Set} → (A → Set) → Set
[ P ] = ∀ {a} → P a

gallais

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds      #-}

import Data.Constraint
import Data.Function

gallais

module Zippy where

data Desc : Set₁ where
  `σ : (A : Set) (d : A → Desc) → Desc
  `r : Desc → Desc
  `q : Desc

open import Size
open import Data.Unit
open import Data.Product

gallais

module Printf

import Lightyear.Char
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%access public export
%default total