JoeyEremondi

-remove-macros je,rg,et
--remove theorem,theoremEnd,proof,proofEnd,align,align*,flalign,flalign*,array,displaymath
--check en
--output html
--replace replacements.txt
--dict dictionary.txt

JoeyEremondi

% !TeX root = main.tex
% !TeX spellcheck = en-US
%%% TeX-command-extra-options: "-shell-escape"

%%
%% This is file `sample-acmsmall.tex',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%

JoeyEremondi

open import Data.Nat.Binary
open import Relation.Binary.PropositionalEquality

plus-zero : ∀ n -> (n + zero) ≡ n
plus-zero zero = refl
plus-zero 2[1+ n ] = refl
plus-zero 1+[2 n ] = refl


plus-suc : ∀ n m -> suc (n + m) ≡ n + (suc m)

JoeyEremondi

module Main

%default total


mutual
  data Code : Nat -> Type where
    N : Code n
    Fn : (c : Code n) -> (el c -> Code n) -> Code n
    Ty : (n : Nat) -> Code (S n) 

JoeyEremondi

(set-logic UF )


(push )

(declare-fun literal_0 () Bool )

(declare-fun literal_1 () Bool )

(declare-fun literal_2 () Bool )

JoeyEremondi

% !Ott args = "-coq_expand_list_types=false -o minirust.tex -o minirust.v"


metavar typvar, X ::=
   {{ coq nat }} {{ coq-equality }}

indexvar n ::=  {{ coq nat }}

grammar

JoeyEremondi

use std::borrow::Borrow;
use std::boxed::Box;

enum Foo {
    Bar,
    Baz,
}

fn compare<T1 : Borrow<Foo>, T2 : Borrow<Foo>>(x : T1, y : T2) -> bool
{

JoeyEremondi

//Definitely NOT valid go, just pseudocode

/** #SESSION TYPE
Buyer
Seller

Buyer.Send(Seller, "BUY")
End
*/

JoeyEremondi

use std::boxed::Box;
use std::rc::Rc;
use std::borrow::Borrow;
use std::mem;

struct BP_REF;
struct BP_BOX;
struct BP_OWNED;
struct BP_RC;

JoeyEremondi

use std::boxed::Box;
use  std::rc::Rc;
use std::borrow::Borrow;
use std::mem;

struct BP_Borrow;
struct BP_RC;


trait BorrowPlus<Borrowed, TRef> : Borrow<Borrowed>