wilcoxjay

Require Import List.
Import ListNotations.

Set Implicit Arguments. 

Module GenHandler. 
  Definition GenHandler (W S O A : Type) : Type := S -> A * S * list W * list O % type.

  Definition ret {W S O A : Type} (a : A) : GenHandler W S O A := fun s => (a, s, [], []).

wilcoxjay

Require Import List.
Require Import String.
Open Scope string_scope.

Definition var := string.

Inductive Expr : Set :=
| EConst                        (* The one and only constant     *)
| EVar (v : var)                (* Variables                     *)
| EApp (e1 : Expr) (e2 : Expr)  (* Application, e1 applied to e2 *)

wilcoxjay

Require Import Arith List Omega Program.
 
Definition fvar : Type := nat. 
Definition bvar : Type := nat. 
 
Inductive sort : Type :=
| N : sort
| ArrowS : sort -> sort -> sort.
 
Definition env := list (fvar * sort).

wilcoxjay

if [ $# -ne 1 ] ; then
  echo Need exactly 1 argument.
  exit 1
fi

lpr -Ujrw12 -Ppsc441 -o fit-to-page -o Duplex=DuplexNoTumble -h "$1"

wilcoxjay

Require Import List.
Import ListNotations.

Section nelist. 
  Variable (A : Type).

Definition nelist : Type := {l : list A | l <> nil}.

Definition safe_head (l : nelist) : A. 
  refine (match proj1_sig l as y' return y' <> [] -> _ with

wilcoxjay

Require Fin.

Theorem fin_1 : 
  forall x : Fin.t 1, 
    x = Fin.F1.
Proof.
  intros.
  destruct x using Fin.caseS'.
  - auto.
  - inversion x.

wilcoxjay

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.

Require Import Omega.

Theorem R_is_plus : 

wilcoxjay

#include "dbg.h"

#include <sys/mman.h>

#include <stdio.h>
#include <stdlib.h>

int main() {
  void* goal_addr = (void*)0x10000;
  size_t length = 1 << 10;

wilcoxjay

Section astrolabe. 
  Variable A : Type.
  Variable open close : A.
  Variable l1 l2 : list A.
  Variable wp : list A -> Prop.

  Goal wp (open :: ((l1 ++ close :: nil) ++ l2)%list) -> 
  wp (open :: (l1 ++ close :: l2)%list) .
    match goal with
    | [ |- ?p ?a -> ?p ?b ] => 

wilcoxjay

Keybase proof

I hereby claim:

• I am wilcoxjay on github.
• I am wilcoxjay (https://keybase.io/wilcoxjay) on keybase.
• I have a public key whose fingerprint is A0D0 8B2A 5F8E F3DE 315D 60A8 78B5 FB36 7E73 831D

To claim this, I am signing this object: