gallais

{-# OPTIONS --without-K #-}

module UIP where

open import Level
open import Relation.Binary.PropositionalEquality

record Canonical {ℓ} {ℓ′} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  field canonical  : A → B
        constraint : ∀ a a′ →  canonical a ≡ canonical a′

gallais

module Even where

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

open ≡-Reasoning

data Even : ℕ → Set where

gallais

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

module Ite where

import Data.Proxy
import GHC.TypeLits

gallais

Inductive Fin : nat -> Type :=
  | Zero : forall n, Fin (S n)
  | Succ : forall n, Fin n -> Fin (S n)
.

Arguments Zero [n].
Arguments Succ [n] k.

Inductive Expr (n : nat) : Type :=

gallais

Set Implicit Arguments.

Require Import Ascii String.

Inductive regex : Set :=
| Emp : regex  
| Eps : regex          
| Chr : ascii -> regex
| Cat : regex -> regex -> regex
| Choice : regex -> regex -> regex

gallais

module StringNat where

open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Data.Unit
open import Data.Bool
open import Data.Product
open import Function

data CharView : Char → Set where

gallais

Require Import NArith.

Fixpoint fac_v1 (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' =>  n * (fac_v1 n')
  end.

Fixpoint visit_fac_v2 (n a : nat) : nat :=
  match n with

gallais

{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module ShowBoth where

import Data.Proxy

gallais

{-# OPTIONS_GHC -fdefer-type-errors #-}
{-# LANGUAGE RankNTypes             #-}

module NumList where

import Data.Void

type NumList a = Num a => [a]

first :: NumList a -> a

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