fehrenbach

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MonadComprehensions   #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RebindableSyntax      #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

fehrenbach

open function

lemma ideminvoid (A : Type)
                 (f : A -> A)
                 (f_idem : forall x, f (f x) = f x)
                 (f_invo : forall x, f (f x) = x)
                 : forall x, f x = id x :=
take x, calc f x = f (f x) : f_idem
             ... = x       : f_invo
             ... = id x    : rfl

fehrenbach

var db = database "links";

var agencies =
  table "agencies"
  with (oid: Int,
        id: Int,
        name: String,
        based_in: String,
        phone: String)
  where oid readonly