gallais

module STLC (Atom : Set) (_≠_ : Atom → Atom → Set) where

open import Data.Empty
open import Data.Product as P hiding (_,_)
open import Data.List 
open import Function hiding (_∋_)

data ★ : Set where
  ι : ★
  _⊳_ : ★ → ★ → ★

gallais

open import Data.String


record Print (A : Set) : Set where
  field
    print : A → String
open Print {{…}} public

mutual
  data α : Set where

gallais

module Sorting where

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary