-- Short Agda tutorial
-- 30 Juni 2016
-- Guest lecture in
--
--   Computer Aided Formal Reasoning (CAFR)
--   Gordon Cichon and Martin Hofmann
--   Summer term 2016
--   Ludwig-Maximilians-University Munich

-- 0. A short tutorial of Agda's data and record types

open import Prelude

-- 1. Tree sort (a functional version of quicksort)
--
-- This first implementation is purely algorithmic.
-- No correctness properties.
-- A very similar program could be written in Haskell.

open import TreeSortBool

-- 2. Tree sort with integrated verification of orderedness.
--
-- Follows paper
--
--   Conor McBride,
--   How to Keep Your Neighbors in Order
--   ICFP 2014

open import TreeSortOrd

-- 3. A refined version of 2.
--
-- Uses Agda's instance arguments to hide all proof passing.
-- The resulting program looks again like 1, only with refined types.

open import TreeSortInstance