Josh Ko josh-hs-ko

josh-hs-ko / FLOLAC18.agda

Last active July 23, 2018 03:59

josh-hs-ko / BinomialHeap.agda

Last active August 29, 2015 14:04

Insertion and extraction in coherence with increment and decrement, and minimum extraction (proved correct, of course).

	open import Data.Sum

	module BinomialHeap (V : Set)
	(_≤_ : V → V → Set) (≤-refl : {x : V} → x ≤ x) (≤-trans : {x y z : V} → x ≤ y → y ≤ z → x ≤ z)
	(_≤?_ : (x y : V) → x ≤ y ⊎ y ≤ x) where

	open import Level using (Level; _⊔_)
	open import Function
	open import Data.Empty
	open import Data.Unit

josh-hs-ko / Shapes-complete.lhs

Created July 10, 2014 12:45

	"Embedded Domain-Specific Languages"
	Jeremy Gibbons, University of Oxford <[email protected]>
	Formosan Summer School on Logic, Languages and Computation, Taipei, July 2014

	Complete solutions for exercises.

	----------------------------------------------------------------------

	> {-# LANGUAGE StandaloneDeriving #-}
	>

josh-hs-ko / Shapes.lhs

Created July 10, 2014 12:44

	"Embedded Domain-Specific Languages"
	Jeremy Gibbons, University of Oxford <[email protected]>
	Formosan Summer School on Logic, Languages and Computation, Taipei, July 2014

	Skeleton code for exercises.

	----------------------------------------------------------------------

	> {-# LANGUAGE StandaloneDeriving #-}
	>

josh-hs-ko / parser.hs

Created July 10, 2014 01:02

Authored by Jeremy Gibbons.

	{-# LINE 30 "parser.ltx" #-}
	{-# LANGUAGE KindSignatures, GADTs #-}
	import Data.List (inits, tails)
	import Data.Char (ord)
	import Control.Monad (mplus)
	{-# LINE 56 "parser.ltx" #-}
	data Grammar :: * where
	Empty :: Grammar
	Unit :: Grammar
	Single :: Char -> Grammar