khibino

Inductive Foo (X : Type) :      Type -> Prop :=
(*                 ^ Parameter  ^ Index *)
| Foo0 : Foo X nat.

Check Foo.


Inductive T0 : Type -> Type -> Prop :=

khibino

data (:|:) f g a = L (f a)
                 | R (g a)

instance (Functor f, Functor g) => Functor (f :|: g) where
  fmap = undefined

instance (Monad f, Monad g) => Monad (f :|: g) where
  return = undefined
  (>>=)  = undefined

khibino

Inductive Mod3' : nat -> Prop :=
| zero' : forall n k, n = 3 * k     -> Mod3' n
| one'  : forall n k, n = 3 * k + 1 -> Mod3' n
| two'  : forall n k, n = 3 * k + 2 -> Mod3' n
.


Lemma nat_mod3' : forall n, Mod3' n.
Proof.
  induction n as [| n1 IHn ].

khibino

import Data.Int (Int32)
import Database.Record.Instances ()
import Database.Relational.Query

hello :: Relation () (Int32, String)
hello =  relation $ return (value 0 >< value "Hello")

world :: Relation () (Int32, String)
world =  relation $ return (value 0 >< value "World!")

khibino

foo :: Kleisli QuerySimple () (Projection Flat (Ex1, Maybe Ex1))
foo =  proc () -> do
  x <- query      -< ex1
  y <- queryMaybe -< ex1
  wheres -< just (x ! eid') .=. y ?! eid'
  returnA -< x >< y

khibino

{-# LANGUAGE FlexibleContexts #-}

module ArrowQuery (
  module Database.Relational.Query,

  query, queryMaybe, query', queryMaybe', wheres, having, groupBy, placeholder,

  relation, relation', aggregateRelation, aggregateRelation',

  QuerySimple, QueryAggregate,

khibino

> {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances #-}
>
> import Data.Int
>
> import Database.Relational.Query
> import Database.Relational.Query.TH
>
>
> $(defineTableDefault defaultConfig
>   "PUBLIC" "my_table"

khibino

{-# LANGUAGE FlexibleContexts #-}

module FirstClassWhere where

import Control.Applicative ((<$>))

import Database.Relational.Query

import Data.Int
import Data.Time

khibino

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Model where

import Data.Int (Int32)

import Data.Time

khibino

import Prelude hiding (sum)

data L1
  = F { ($$) :: L1 -> L1 }
  | V { unV :: Int }

infixl 1 $$

instance Show L1 where