enn

%default total
-- because we're doing proofs

-- This file demonstrates a simple example of proof by reflection
-- mentioned in: http://ftp.science.ru.nl/CompMath.Found/buchberger.pdf

infix 5 <-->

(<-->) : Type -> Type -> Type
p <--> q = (p -> q, q -> p)

enn

module PEG (
  Parse(..),
  eofP, charP, strP, anyOfP, anyButP, anyP, followedP, notFollowedP, ifP, emptyP, optP, repeatP, repeatP1, choiceP, seqP
) where

-- http://d.hatena.ne.jp/Otter_O/20090207/1233991312

import Data.List (intercalate)

ifNothing Nothing v = Just v