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

gallais

module scope where

import Level as L
open import Data.Nat.Base
open import Data.Vec hiding (_>>=_)
open import Data.Fin.Base
open import Data.String
open import Data.Maybe as Maybe
open import Data.Product as Prod
open import Relation.Nullary

gallais

open import Level
open import Data.List.Base hiding (filter)
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Function
open import Relation.Nullary
open import Relation.Unary

module _ {a} {A : Set a} where

gallais

open import Relation.Nullary
open import Agda.Builtin.Equality

data X : Set where
  a b c : X

firstA : (x y z : X) → X
firstA a y z = a
firstA x a z = a
firstA x y a = a

gallais

module Container

%default total

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

container : Container -> Type -> Type