dnbln

Require Import Nat.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.
Require Import Lia.


Inductive Exp : Set :=
    | Const (_: nat) : Exp
    | Add (_: Exp) (_: Exp) : Exp
    | Mul (_: Exp) (_: Exp) : Exp.

dnbln

import os

COPY = True
RUST_CHECKOUT = "path/to/rust/checkout"

tests = []

def collect_tests(dir):
    for root, dirs, files in os.walk(dir, topdown=False):
        for name in files:

dnbln

Sandbox we will have to break out from:

function moonbars.getEnvironment()
    return {
        -- irrelevant stuff
        loadstring = loadstring,
        -- irrelevant stuff
        string = {
            byte = string.byte,

dnbln

trait X: Copy {
    fn new() -> Self;
}

trait Y<A, B> {
    fn x(&mut self, x: A) -> B;
}

struct S<A: X> {
    m: BTreeMap<usize, A>,

dnbln

use std::{
    borrow::Cow,
    ops::{Range, RangeInclusive},
};

#[derive(Default, Debug, Clone)]
pub struct Programmer<'a> {
    pub about_me: AboutMe<'a>,
    pub languages: Vec<Language<'a>>,
    pub technologies: Vec<TechnologyCategory<'a>>,

dnbln

const ROOT_LINK: &str = "https://api.example.com";

// macro to generate urls for an endpoint from root, path (fmt string) and args
macro_rules! ep {
    ($ep:literal $($args:tt)*) => {
        format!(concat!("{}", $ep), ROOT_LINK, $($args)*)
    }
}

// example usage

dnbln

fn main() {
    let mut board = [
                             [3, 0, 6,  5, 0, 8,  4, 0, 0],
                             [5, 2, 0,  0, 0, 0,  0, 0, 0],
                             [0, 8, 7,  0, 0, 0,  0, 3, 1],

                             [0, 0, 3,  0, 1, 0,  0, 8, 0],
                             [9, 0, 0,  8, 6, 3,  0, 0, 5],
                             [0, 5, 0,  0, 9, 0,  6, 0, 0],

dnbln

#include <iostream>

int sudoku_m[9][9] = {
    {3, 0, 6,  5, 0, 8,  4, 0, 0},
    {5, 2, 0,  0, 0, 0,  0, 0, 0},
    {0, 8, 7,  0, 0, 0,  0, 3, 1},

    {0, 0, 3,  0, 1, 0,  0, 8, 0},
    {9, 0, 0,  8, 6, 3,  0, 0, 5},
    {0, 5, 0,  0, 9, 0,  6, 0, 0},

dnbln

.equ BUF_SIZE, 131072

.global _start
_start:
	# argc = (%rsp)
	# argv = %rsp+8

	# argc *= 8
	shlq $3, (%rsp)
	

dnbln

#!/bin/sh

if [[ -d $1 ]]
then
	printf "$1 deja exista\n" 1>&2
	exit 1
fi

mkdir $1