{-# OPTIONS --rewriting #-}

-- Formalization of "The directed plump ordering" by Daniel Gratzer,
-- Michael Shulman, and Jonathan Sterling. The formalization was
-- carried out by Jonathan Sterling and Daniel Gratzer.

-- The code presented here can also be accessed at
-- https://github.com/jonsterling/agda-directed-plump-ordering.

module index where

import Preamble
import Ordering