wilcoxjay

\version "2.18.2"
\relative c'' {
  <<
    { g4( f) } \\
    { e4( d) }
  >>
}

wilcoxjay

Require Import Reals.
Open Scope R_scope.
Axiom differentiate : (R -> R) -> (R -> R).
Notation "'d' e | x" := (differentiate (fun x => e)) (at level 50).
Goal d 2 * x | x = fun x => 2.

wilcoxjay

Axiom foo : nat -> nat -> Prop.
Notation "'d' x | y" := (foo x y) (at level 100).
Goal foo (10 + 7) 14.

wilcoxjay

Require Vector.

Module Type NAT.
  Parameter n : nat.
End NAT.

Module A (N : NAT).
  Definition t : Type := Vector.t unit N.n.
End A.

wilcoxjay

msg := Put(k,v) | Get(k) | Resp(v_old)

Server: 
  main():
    db = {}
    while m = recv():
      v0 = db[m.k]
      if m is Put: 
        db[m.k] = m.v
      send Resp(v0) to m.src

wilcoxjay

Require Import List.
Import ListNotations.

Set Implicit Arguments.
Set Maximal Implicit Insertion.

Module tree.
  Section tree.
    Variable A : Type.

wilcoxjay

Require Import List Arith.


Axiom cand : Type.
Axiom cand_eqb : cand -> cand -> bool.
Axiom edge : cand -> cand -> nat.

Definition bool_in (p: (cand * cand)%type) (l: list (cand * cand)%type) :=
  existsb (fun q => (andb (cand_eqb (fst q) (fst p))) ((cand_eqb (snd q) (snd p)))) l. 

wilcoxjay

Require Import List.
Import ListNotations.

Fixpoint akr_fold {A} (P : nat -> Type) (P_nil : P 0) (P_cons : forall n, A -> P n -> P (S n)) (l : list A) : P (length l) := 
  match l with
  | [] => P_nil
  | a :: l' => P_cons _ a (akr_fold P P_nil P_cons l')
  end.

wilcoxjay

Require Import List.
Import ListNotations.

Module member.
  Inductive t {A : Type} (x : A) : list A -> Type :=
  | Here : forall {l}, t x (x :: l)
  | There : forall {y l}, t x l -> t x (y :: l)
  .
  Arguments Here {_ _ _}.
  Arguments There {_ _ _ _} _.

wilcoxjay

Fixpoint Fin (n : nat) : Type :=
  match n with
  | 0 => Empty_set
  | S n' => option (Fin n')
  end.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin n) (g : Fin n -> A),
    (forall x, g (f x) = x) /\ (forall y, f (g y) = y).