xekoukou

module test where

module QBree (A : Set) where

  data Bree : Set where
    _∪_ : Bree → Bree → Bree

  data S : Bree → Bree → Set where
    assoc   : (x y z : Bree) → S (x ∪ (y ∪ z)) ((x ∪ y) ∪ z)

xekoukou

module test where

open import Agda.Builtin.Reflection
open import Reflection
open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Unit
open import Prelude.List

xekoukou

module test where

open import Reflection
open import Agda.Builtin.Reflection
open import Agda.Builtin.Word
open import Agda.Builtin.Float
open import Agda.Builtin.Char
open import Prelude.List
open import Prelude.Maybe
open import Prelude.Nat

xekoukou

module gog where

open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning


data ℕ : Set where
  z : ℕ

xekoukou

module HL5 where


open import Agda.Builtin.Unit
import Level as L

postulate
  World : Set

xekoukou

registered phi for shadowing
New checkpoint {
  old = 0
  new = 32
  sub = wkS 1 idS
  cxt = (phi : Agda.Primitive.Cubical.I)
  old substs = 0 :  idS
  new substs =
    0 :  wkS 1 idS
    32 :  idS

xekoukou

{-# OPTIONS --verbose tc.constr:1000 #-}
module test2 where

open import Reflection
open import Agda.Builtin.Reflection
open import Prelude.Nat
open import Prelude.Unit
open import Prelude.Equality
open import Prelude.Function
open import Prelude.List

xekoukou

open import Data.Unit

postulate
  World : Set

HVet : Set₁
HVet = World → Set

variable
  HQ : HVet 

xekoukou

data Bool : Set where
  true : Bool
  false : Bool

data D : Set where
  d : D

data E : Set where
  e : E

xekoukou

data K : Set where

WSet : Set₁
WSet = K → Set

variable
  HW HQ : WSet