nkaretnikov

# Part of configuration.nix

  # Mix left and right channels.
  sound.extraConfig =
    ''
    pcm.!default {
        type plug
        slave.pcm {
            type asym
            playback.pcm {

nkaretnikov

(** Recall the function [forallb], from the exercise
    [forall_exists_challenge] in chapter [Poly]: *)

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
    | [] => true
    | x :: l' => andb (test x) (forallb test l')
  end.

(** Using the property [all], write down a specification for [forallb],

nkaretnikov

(** **** Exercise: 3 stars (all_forallb) *)
(** Inductively define a property [all] of lists, parameterized by a
    type [X] and a property [P : X -> Prop], such that [all X P l]
    asserts that [P] is true for every element of the list [l]. *)

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=
  | all_nil : all X P []
  | all_cons : forall (x : X) (xs : list X),
                 P x -> all X P xs -> all X P (x :: xs).

nkaretnikov

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  intros.
  unfold excluded_middle in H.
  unfold "~" in H0.
  unfold "~" in H.
(* 1 subgoals, subgoal 1 (ID 72) *)

nkaretnikov

(** One more quick digression, for adventurous souls: if we can define
    parameterized propositions using [Definition], then can we also
    define them using [Fixpoint]?  Of course we can!  However, this
    kind of "recursive parameterization" doesn't correspond to
    anything very familiar from everyday mathematics.  The following
    exercise gives a slightly contrived example. *)

(** **** Exercise: 4 stars, optional (true_upto_n__true_everywhere) *)
(** Define a recursive function
    [true_upto_n__true_everywhere] that makes

nkaretnikov

This query

INSERT INTO "event_user_notification_sent" (
    "id", "ts", "notification"
) (
    SELECT "id", "ts", "notification"
	FROM "event_notification_sent"
	WHERE "id" IN (
        SELECT "id"

nkaretnikov

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0 
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

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
);

nkaretnikov

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

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

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