tbelaire

m : mname
H_dir : directed_ct nil
H_noobj : Object \notin dom nil

======================== ( 1 / 2 )
eq_rect_r (fun C : cname => ok_type_ nil C -> option cname)
  (fun _ : ok_type_ nil Object => None) (ok_nil_object Object (ok_obj nil))
  (ok_obj nil) = None
  
Proof.

tbelaire

P : cname -> Type
P_Obj : P Object
P_Ind : forall (C D : cname) (fs : flds) (ms : mths),
        ok_type_ nil D -> binds C (D, fs, ms) nil -> P D -> P C
H_ok : ok_type_ nil Object

======================== ( 1 / 1 )
match
  match
    match H_ok in (ok_type_ _ t) return (t = Object) with

tbelaire

(**************************************************************)
(** * Coq for POPL Folk *)
(**************************************************************)

(** A streamlined interactive tutorial on fundamentals of Coq,
    focusing on a minimal set of features needed for developing
    programming language metatheory.

    Mostly developed by Aaron Bohannon, with help from Benjamin
    Pierce, Dimitrios Vytiniotis, and Steve Zdancewic.

tbelaire

Makefiles, here's how to use them.
What's a Kernel Module:
    Adventures in getting the 360 controller light to stop spinning
Racket Macros
Racket Match: Never use first/rest again.
Rust: Borrows
Rust: Send + Sync gives you thread safety for free
Rust in the Kernel.
Coq: an introduction to induction
Creating VTables in C for fun and profit (and dynamic dyspatch :P)

tbelaire

Inductive wf: envmode -> env typ -> env typ -> env val -> Prop :=
| wf_empty: forall m, wf m empty empty empty
| wf_push: forall m e1 e2 s x T v,
    wf m e1 e2 s ->
    x # e1 ->
    x # s ->
    ty_trm ty_precise sub_general (get_ctx m e1 e2) (get_sigma m e1 e2) (trm_val v) T ->
    wf m (e1 & x ~ T) e2 (s & x ~ v).

Definition wf_stack (G: ctx) (S: sigma) (s: stack): Prop :=

tbelaire

Inductive Nat :=
| Z : Nat
| S : Nat -> Nat.

Fixpoint plus (x : Nat) (y : Nat) : Nat :=
    match x with
    | Z => y
    | S x' => S (plus x' y)
    end.

tbelaire

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top") -*- *)
(* File reduced by coq-bug-finder from original input, then from Coq.Lists.List70 lines, Coq.Arith.Max lines to 97 lines, then from 197 lines to 115 lines, then from 129 lines to 115 lines *)
(* coqc version 8.4pl6 (October 2015) compiled on Oct 12 2015 11:33:25 with OCaml 4.02.3
   coqtop version 8.4pl6 (October 2015) *)
Require Coq.Lists.List.
Require Coq.Arith.Max.

Module Type ATOM.

  Parameter atom : Set.

tbelaire

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top") -*- *)
(* File reduced by coq-bug-finder from original input, then from Coq.Lists.List70 lines, Coq.Arith.Max lines to 97 lines, then from 197 lines to 115 lines, then from 129 lines to 115 lines *)

Require Coq.Lists.List.
Require Coq.Arith.Max.
Require Coq.Arith.Peano_dec.

Module Type ATOM.

  Parameter atom : Set.

tbelaire

/* automatically generated by rust-bindgen */

pub type __int128_t = ::std::os::raw::c_void;
pub type __uint128_t = ::std::os::raw::c_void;
pub type __builtin_va_list = [__va_list_tag; 1usize];
#[repr(C)]
#[derive(Copy)]
pub struct Struct_ftrace_branch_data {
    pub func: *const ::std::os::raw::c_char,
    pub file: *const ::std::os::raw::c_char,

tbelaire

   Compiling bindgen v0.16.0 (https://github.com/alexander255/rust-bindgen.git#88c54e09)
     Running `rustc /home/tbelaire/.multirust/toolchains/nightly/cargo/git/checkouts/rust-bindgen-32f69e0092dfc21d/master/build.rs --crate-name build_script_build --crate-type bin -g --out-dir /home/tbelaire/Code/rust.ko/target/debug/build/bindgen-317dda2c0a25a7ba --emit=dep-info,link -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps --cap-lints allow`
   Compiling rustc-serialize v0.3.19
     Running `rustc /home/tbelaire/.multirust/toolchains/nightly/cargo/registry/src/github.com-88ac128001ac3a9a/rustc-serialize-0.3.19/src/lib.rs --crate-name rustc_serialize --crate-type lib -g -C metadata=3bc953984ed46e7f -C extra-filename=-3bc953984ed46e7f --out-dir /home/tbelaire/Code/rust.ko/target/debug/deps --emit=dep-info,link -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps --cap-lints allo