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

open import Agda.Builtin.Size
open import Data.Maybe.Base

data List {n} (T : Set n) (i : Size) : Set n where
  [] : List T i
  _∷_ : ∀ {j : Size< i} → T → List T j → List T i

data Smaller {n} (T : Size → Set n) (i : Size) : Set n where
  [_] : {j : Size< i} → T j → Smaller T i

gallais

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

module SyntaxDesc (I : Set) where

open import Agda.Primitive using () renaming (Set to Type)
open import Data.Nat.Base
open import Data.Fin.Base
open import Data.List.Base using (List; []; _∷_; _++_)

data Desc : Type₀ where

gallais

Require Import List.

Inductive PalAcc {A : Type} (acc : list A) : list A -> Type
  := Even : PalAcc acc acc
   | Odd  : forall x, PalAcc acc (x :: acc)
   | Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs)
.

Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs.

gallais

Inductive Tree (A : Set) : Set :=
  | Leaf : A -> Tree A
  | Node : bool -> Tree A * Tree A -> Tree A.

Definition subTree {A : Set} (b : bool) (lr : Tree A * Tree A) : Tree A :=
  match (b, lr) with
    | (true, (a, b)) => a
    | (false, (a, b)) => b
  end.

gallais

data EventT : (event : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  MkEventTCont : (event -> m (EventT event m a)) -> EventT event m a
  MkEventTTerm : m a -> EventT event m a
  MkEventTEmpty : EventT event m a

data LAM : (x : Type) -> Type where
  App : x -> x -> LAM x
  Lam : (x -> x) -> LAM x

LC : Type

gallais

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat hiding (_+_; _<_)

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Binary


-- C-c C-z RET _*_ _≡_ RET

gallais

open import Data.List using (List); open List
open import Data.List.Properties
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private variable A : Set

gallais

open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product

variable
  m n : ℕ
  b : Bool
  Γ Δ Ξ T I O : Vec Bool n

gallais

open import Size
open import Codata.Thunk

data BinaryTreePath (i : Size) : Set where
  here : BinaryTreePath i
  branchL : Thunk BinaryTreePath i → BinaryTreePath i
  branchR : Thunk BinaryTreePath i → BinaryTreePath i

zero : ∀ {i} → BinaryTreePath i
zero = branchL λ where .force → zero