JoeyEremondi

[DEBUG websocat] Done third phase of interpreting options.
[INFO  websocat::net_peer] Resolving hostname to IP addresses
[INFO  websocat::net_peer] Got IP: 127.0.0.1:7979
[DEBUG websocat] Done fourth phase of interpreting options.
[DEBUG websocat] Preparation done. Now actually starting.
[DEBUG websocat::sessionserve] Serving WsServer(TlsAccept(TcpListen(127.0.0.1:7878))) to TlsConnect(TcpConnect([127.0.0.1:7979])) with Options { websocket_text_mode: false, websocket_protocol: None, websocket_reply_protocol: None, udp_oneshot_mode: false, udp_broadcast: false, udp_multicast_loop: false, udp_ttl: None, udp_join_multicast_addr: [], udp_join_multicast_iface_v4: [], udp_join_multicast_iface_v6: [], udp_reuseaddr: false, unidirectional: false, unidirectional_reverse: false, max_messages: None, max_messages_rev: None, exit_on_eof: true, oneshot: false, unlink_unix_socket: false, unix_socket_accept_from_fd: false, exec_args: [], ws_c_uri: "ws://0.0.0.0/", linemode_strip_newlines: false, linemode_strict: false, origi

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;