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:
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, [], []). |
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 *) |
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). |
if [ $# -ne 1 ] ; then | |
echo Need exactly 1 argument. | |
exit 1 | |
fi | |
lpr -Ujrw12 -Ppsc441 -o fit-to-page -o Duplex=DuplexNoTumble -h "$1" |
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 |
Require Fin. | |
Theorem fin_1 : | |
forall x : Fin.t 1, | |
x = Fin.F1. | |
Proof. | |
intros. | |
destruct x using Fin.caseS'. | |
- auto. | |
- inversion x. |
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 : |
#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; |
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 ] => |
I hereby claim:
To claim this, I am signing this object: