gallais

module Error

export
data Error : (err, a : Type) -> Type where
  MkError : (forall r. (err -> r) -> (a -> r) -> r) -> Error err a

export %inline
runError : Error err a -> (err -> r) -> (a -> r) -> r
runError (MkError hdl) kE kV = hdl kE kV

gallais

module LambdaLetRec

import Data.List1
import Data.List.Quantifiers

--------------------------------------------------------------------------------
-- types

infixr 5 ~>

gallais

import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality

%default total

toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2

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