tbelaire

	.section	".init"
	.global     _start
	.align
	.arm
@---------------------------------------------------------------------------------
_start:
@---------------------------------------------------------------------------------
	b	rom_header_end

	.fill   156,1,0			@ Nintendo Logo Character Data (8000004h)

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);
// }

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);
// }

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

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

#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

use std::marker::PhantomData;

enum True {}
enum False {}

enum ModeX {}

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

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

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

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.