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.

Set Implicit Arguments.
Set Maximal Implicit Insertion.

Module tree.
  Section tree.
    Variable A : Type.

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 Vector.

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

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

wilcoxjay

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

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

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

wilcoxjay

(Prog [
(Func "swap" ("a" :: "i" :: "j" :: nil)
  (Sseq 
  (Sset "tmp" (Eidx (Evar "a") (Evar "i")))
  (Sseq 
  (Swrite "a" (Evar "i") (Eidx (Evar "a") (Evar "j")))
  (Swrite "a" (Evar "j") (Evar "tmp"))))
  (Evar "a"));
(Func "reverse" ("a" :: nil)
  (Sseq 

wilcoxjay

Theorem foo : [(n : nat) -> (x : =(zero; succ(n); nat)) -> =(zero; succ(n); nat)] {
  intro; aux {auto};
  intro; aux {auto};
  hypothesis #2  ||| works just fine here
}.

Operator is-zero : (0).
[is-zero(n)] =def= [natrec(n; unit; _._. void)].

Theorem succ-not-zero : [(n : nat) -> =(succ(n); zero; nat) -> void] {

wilcoxjay

-*- mode: compilation; default-directory: "~/build/JonPRL/" -*-
Compilation started at Thu Oct  6 17:42:16

/Users/jrw12/build/JonPRL/bin/jonprl --check bug.jonprl
In assert, goal is:
⊢ =(nat; nat; U{i})
z = h@101
term = void
term' = void
In assert, goal is: