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

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

Inductive ev : nat -> Prop :=
| ev_0  : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).


Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
Proof.
  intros n m H1 H2.
  induction H1.
  auto.

tbelaire

Inductive tm_helper : bool -> Set :=
| tm_true {b: bool} : tm_helper b
| tm_false {b: bool} : tm_helper b
| tm_if {b: bool} : tm_helper b -> tm_helper b ->
        tm_helper b -> tm_helper b
| tm_zero {b: bool} : tm_helper b
| tm_succ {b: bool} : tm_helper b -> tm_helper b
| tm_pred {b: bool} : tm_helper b -> tm_helper b
| tm_iszero {b: bool} : tm_helper b -> tm_helper b

tbelaire

#![allow(non_snake_case)]
extern crate argparse;


use argparse::{ArgumentParser, StoreTrue, Store};

use std::fs::File;
use std::str::FromStr;
use std::io::{BufReader, BufRead};

tbelaire

use std::marker::PhantomData;

enum True {}
enum False {}

enum ModeX {}

#[derive(Debug)]
struct Built<M> {
    int: i32,

tbelaire

#include <stdio.h>

int main() {
    char word[4] = {1, 2, 3, 4};
    int* xptr = (int*)(&word[0]);
    printf ("x is %d\n", *xptr);
    printf ("x low byte %d\n", *xptr & 0xFF);
    printf ("x 2nd byte %d\n", *xptr >> 8 & 0xFF);
    printf ("x 3rd byte %d\n", *xptr >> 16 & 0xFF);
    printf ("x 4th byte %d\n", *xptr >> 24 & 0xFF);

tbelaire

module Main where
import Control.Monad.State
--import Control.Monad.Cont
--import Data.List ((\\))

[] \\ ys = []
xs \\ [] = xs
(x:xs) \\ ys | x `elem` ys = xs \\ ys
             | otherwise   = x :(xs \\ ys)

tbelaire

module Graph where
-- type String = [Char]

-- Problem, we have a graph
type Graph a = ([a], [(a, [a])])


g :: Graph Char
g = ("abc", [('a', "bc"), ('b', "c"), ('c', "a")])

tbelaire

#![feature(intrinsics, lang_items, no_std)]

#![no_std]
#![crate_type = "staticlib"]

// // Declare some intrinsic functions that are provided to us by the compiler.
// extern "rust-intrinsic" {
//     fn overflowing_add<T>(a: T, b: T) -> T;
//     fn u32_sub_with_overflow(x: u32, y: u32) -> (u32, bool);
// }