nkaretnikov

Inductive pal {X : Type} : (list X) -> Prop :=
  | p_nil : pal nil
  | p_one : forall x : X, pal [x]
  | p_rec : forall (x : X) (xs : list X), pal xs -> pal (x :: xs ++ [x]).

Example pal_1_2_3_4_4_3_2_1 : pal [1;2;3;4;4;3;2;1].
Proof.
  apply (p_rec 1 [2; 3; 4; 4; 3; 2]).
  apply (p_rec 2 [3; 4; 4; 3]).
  apply (p_rec 3 [4; 4]).

nkaretnikov

subseq :: Eq a => [a] -> [a] -> [a]
subseq xs ys = let res = go xs ys
               in if res /= xs then [] else res
  where
    go _         []        = []
    go []        _         = []
    go xs@(x:xt) ys@(y:yt)
      | x  ==  y  = x : go xt yt
      | otherwise = go xs yt

nkaretnikov

Inductive subseq {X : Type} : (list X) -> (list X) -> Prop :=
  | s_nil : forall (xs : list X),
              subseq nil xs
  | s_diff : forall (y : X) (xs ys : list X),
              subseq xs ys -> subseq xs (y::ys)
  | s_same : forall (x : X) (xs ys : list X),
              subseq xs ys -> subseq (x::xs) (x::ys).

(*
subseq [1,2,3] [1,2,3]:

nkaretnikov

with (import <nixpkgs> {}).pkgs;
let haskellPackages' = haskellngPackages.override {
      overrides = self: super: {
        tasty = self.callPackage ../core {};
      };
    };
    pkg = haskellPackages'.callPackage
            ({ mkDerivation, base, cabal-install, pcre-light, QuickCheck
             , stdenv, tagged, tasty, tasty-hunit
             }:

nkaretnikov

Instead of:

UserNotificationPref
    user     UserId
    project  ProjectId            Maybe
    type     NotificationType
    delivery NotificationDelivery

There'll be two tables:

nkaretnikov

Theorem Sx_le_Sx_y : forall x y, S x <= S (x + y).
Proof.
  induction y as [|y'].
  Case "y' = 0".
    rewrite <- plus_n_O.
    apply le_n.
  Case "y' = S y".
    apply le_S.
    rewrite <- plus_n_Sm.
    apply IHy'.

nkaretnikov

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
  induction n as [|n'].
  Case "n' = 0".
    intros.
    induction m as [|m'].
    SCase "m' = 0".
      apply le_n.
    SCase "m' = S m".

nkaretnikov

 id | user |     type      | delivery 
----+------+---------------+----------
  1 |    1 | NotifReply    | Website
  2 |    1 | NotifReply    | Email
  3 |    2 | NotifRethread | Website
  4 |    3 | NotifWiki     | Website
  5 |    3 | NotifWiki     | Email

nkaretnikov

function transparentWrapping(f) {
	return function() {
		return f.apply(null, arguments);
	};
}

function add3(x, y, z) {
	return x + y + z;
}

nkaretnikov

-- Create the needed tables.
CREATE TABLE "project_notification" (
    "id" SERIAL PRIMARY KEY UNIQUE NOT NULL,
    "created_ts" TIMESTAMP WITH TIME ZONE NOT NULL,
    "type" VARCHAR NOT NULL,
    "to" INT8 NOT NULL,
    "project" INT8 NOT NULL,
    "content" VARCHAR NOT NULL,
    "archived" BOOLEAN NOT NULL
);