gallais

module Rot13 where

import Control.Monad (guard)
import Data.Char (ord, chr, toLower, isLower)
import Data.Function (on)
import Data.List (sortBy)
import Data.Maybe (mapMaybe)

import Data.Set (Set)
import qualified Data.Set as Set

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