myuon

import Control.Monad
import Control.Monad.Fix
import Control.Monad.Primitive
import Control.Monad.ST
import Data.Primitive.MutVar
import qualified Data.Vector as V
import qualified Data.Vector.Generic.Mutable as VM
import qualified Data.Vector.Unboxed.Mutable as VUM
import qualified Data.Vector.Unboxed as VU
import Data.List

myuon

portals@me

要件をアレする

• SLA: 99.9%
• インフラコスト: (固定費$10 + $1/ユーザー)/月
• ターゲット: クリエイター層(PCメイン) + ファン層(PC or スマホ)

エンティティ

myuon

theory LTL
  imports Main
begin

datatype 'a LTL
  = Latom 'a
  | Ltrue
  | Lor "'a LTL" "'a LTL" (infixl "∨t" 81)
  | Lnot "'a LTL" ("¬t _" [85] 85)
  | Lnext "'a LTL" ("○ _" [88] 87)

myuon

# 学生向けアルバイトらしき何かの募集のお知らせ

目的: 優秀な若者が進捗をしているのを横で見たいので進捗を報告してもらってその分のお金を払うみたいな実験をやってみようと思います。

お仕事フロー:
- 仕事内容を相談により決定します。応募者の方でやりたいことがある場合はそれになるべく沿うつもりですが、必ず成果が定量的に測れるものにしたいと思っています。
- 仕事をします。
- 週1回程度、成果を報告していただきます。音声チャット等がメインになると思います。次の週にどこまで作業を進めるかの宣言も行います。(到達できなくとも特にペナルティはありません)
- 月1回など決まったタイミングで謝礼金相当のものをお支払いします。口座振り込みかamazonウィッシュリストから現物支給かご飯を奢られるか好きなものをお選びください。
- どちらかが辞めたいとなったら契約は終了です。

myuon

#[macro_use] extern crate macro_attr;
#[macro_use] extern crate bmp;
use std::fs;
use std::mem;
use std::io::{BufWriter, Write};
use std::iter;
use bmp::{Image, Pixel};

trait Serialize where Self: Sized {
    fn serialize(&self) -> Vec<u8>;

myuon

theory ListPiyo
imports Main
begin

datatype 'a list = nil | cons 'a "'a list"

primrec append where
    "append nil ys = ys"
|   "append (cons x xs) ys = cons x (append xs ys)"

myuon

~$ tree -L 1
.
├── cubism-js
├── dist
├── node_modules
├── package-lock.json
├── package.json
├── src
    └── tsc
        └── main.ts   

myuon

theory cantor
  imports Main
begin

definition map :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
  "map A B = {f. \<forall>a\<in>A. f a \<in> B}"

definition surj where
  "surj A B f = (f \<in> map A B \<and> (\<forall>b\<in>B. \<exists>a\<in>A. f a = b))"

myuon

theory qsort
imports Main
begin

fun qsort :: "nat list ⇒ nat list" where
  "qsort [] = []"
| "qsort (x#xs) = qsort [y←xs. y < x] @ [x] @ qsort [y←xs. x ≤ y]"

inductive inc :: "nat list ⇒ bool" where
  inc_nil: "inc []"

myuon

theory Trans
imports Main
begin
(* "Lectures on the Curry-Howard Isomorphism"  Lemma 1.4.2 *)

inductive star :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
lift: "r x y ⟹ star r x y" |
trans: "star r x y ⟹ star r y z ⟹ star r x z"

inductive trans_list :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for r where