yuga

Oracle:
http://docs.oracle.com/cd/B19306_01/server.102/b14200/sql_elements003.htm#BABGIGCJ

PostgreSQL:
http://www.postgresql.org/docs/9.1/static/datatype-datetime.html

MySQL:
http://dev.mysql.com/doc/refman/5.0/en/date-and-time-literals.html

DB2 v9.5

yuga

account1'' :: Relation () Account1
account1'' = relation $ do
  a  <- query account
  wheres $ a ! Account.productCd' `in'` values ["CHK", "SAV", "CD", "MM"]
  return $ Account1 |$| a ! Account.accountId'
                    |*| a ! Account.productCd'
                    |*| a ! Account.custId'
                    |*| a ! Account.availBalance'

data Account1 = Account1

yuga

HSQL
--------------------
DB.HSQL.SQLite3

HDBC
--------------------
Database.HDBC.Sqlite3

HDBI
--------------------

yuga

module decimal

record Decimal : Nat -> Type where
  MkDecimal : (places : Nat) -> (mantissa : Integer) -> Decimal places

signum : Integer -> Integer
signum n = case compare n 0 of
                LT => (-1)
                EQ => 0
                GT => 1

yuga

-- > chunkGroupBy (\x y -> x == y) 6 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0]],[[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 7 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0],[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 15 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0],[1,1,1],[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 16 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]

yuga

#!/bin/bash

PRG=$(readlink -f "$0")
PRGDIR=$(dirname "${PRG}")

set -x
set -e

list=(
haskell-names-th_0.0.1.0.dsc

yuga

Definition five_not_even' : ~ ev 5 :=
  fun (Hev5 : ev 5) =>
    (fun (P : nat -> Prop)                                       (* evの帰納法の原理*)
         (f : P 0)
         (f0 : forall n : nat, ev n -> P n -> P (S (S n))) =>
            fix F (n : nat) (e : ev n) {struct e} : P n :=       (* eについて減少 *)
              match e in (ev n0) return (P n0) with
              | ev_0 => f
              | ev_SS n1 ev1 => f0 n1 ev1 (F n1 ev1)
              end)

yuga

class Producer p where
     get :: Resource r => p -> r

class Resource a where
     fire :: a -> Int

data A = A Int
data B = B Int

instance Producer A where

yuga

(*  **** Exercise: 1 star (bool_prop) *)
(** **** 練習問題: ★ (bool_prop) *)
Theorem andb_false : forall b c,
  andb b c = false -> b = false \/ c = false.
Proof.
  intros b c H.
  unfold andb in H.
  destruct b.
    right. apply H.
    left. reflexivity.

yuga

module Printf

%default total

data Format = FInt Format -- %d
            | FString Format -- %s
            | FOther Char Format -- [a-zA-Z0-9]
            | FEnd --

format : List Char -> Format