Skip to content

Instantly share code, notes, and snippets.

View Instance.agda
open import Data.String
record Print (A : Set) : Set where
field
print : A String
open Print {{…}} public
mutual
data α : Set where
View STLC.agda
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
ι :
_⊳_ :
View Sorting.agda
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