gallais

module Compiled-252 where

data U : Set where
  z : U
  s : U → U

{-# IMPORT Compiled.URaw #-}
{-# COMPILED_DATA U Compiled.URaw.U Compiled.URaw.Z Compiled.URaw.S #-}

gallais

open List

let bind (xs : 'a list) (f : 'a -> 'b list) : 'b list =
  concat (map f xs)

let rec parts : 'a list -> 'a list list list = function
  | []      -> [[]]
  | [c]     -> [[[c]]]
  | c :: cs ->
    bind (parts cs) (fun (p :: ps) ->

gallais

record Default {ℓ} (A : Set ℓ) (a : A) : Set ℓ where
  constructor _!
  field value : A

instance

  default : ∀ {ℓ} {A : Set ℓ} a → Default A a
  default a = record { value = a }

open import Agda.Builtin.Nat

gallais

module Subst1 where
open import Term

infixl 20 _-_
_-_ : {σ : Ty} → (Γ : Con) → Var Γ σ → Con
ε - ()
(Γ , σ) - vz = Γ
(Γ , τ) - vs x = (Γ - x) , τ

gallais

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
-- We need undecidable instances for the definition of @Foldr@,
-- and @Domains@ and @CoDomain@ using @If@ for instance.

gallais

module Printf

import Lightyear.Char
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%access public export
%default total

gallais

module Zippy where

data Desc : Set₁ where
  `σ : (A : Set) (d : A → Desc) → Desc
  `r : Desc → Desc
  `q : Desc

open import Size
open import Data.Unit
open import Data.Product

gallais

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds      #-}

import Data.Constraint
import Data.Function

gallais

module Accessibility where

data Acc {A : Set} (R : A → A → Set) (a : A) : Set where
  step : (∀ b → R b a → Acc R b) → Acc R a 

□^ : ∀ {A : Set} (R : A → A → Set) → (A → Set) → (A → Set)
□^ R P a = ∀ b → R b a → P b

[_] : {A : Set} → (A → Set) → Set
[ P ] = ∀ {a} → P a

gallais

module poc.FiniteMap where

open import Function
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

record _↔_ (A B : Set) : Set where
  field push : A → B
        pull : B → A