Skip to content

Instantly share code, notes, and snippets.

View gallais's full-sized avatar

G. Allais gallais

View GitHub Profile
@gallais
gallais / STLC.agda
Last active September 8, 2016 11:01 — forked from useronym/STLC.agda
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 Instance.agda
open import Data.String
record Print (A : Set) : Set where
field
print : A → String
open Print {{…}} public
mutual
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