314maro

#include <iostream>
#include <vector>
#include "vm.hpp"

int main() {
  const unsigned char offset = 0x03, loopend = 0x27;
  // 0x00:ptr, 0x01:pc, 0x02:len
  std::vector<unsigned char> inst =
    { 0x02, 0x00, 0x02, 0x00, 0x10 // store
    , 0x02, 0x01, 0x02, offset, 0x10 // store

314maro

Module Q11.
  Require Import Arith.
  Fixpoint sum_odd(n:nat) : nat :=
    match n with
    | O => O
    | S m => 1 + m + m + sum_odd m
    end.

  Goal forall n, sum_odd n = n * n.
  Proof.

314maro

Module Q6.
  Require Import Arith.

  Goal forall x y, x < y -> x + 10 < y + 10.
  Proof.
    intros.
    apply plus_lt_compat_r.
    assumption.
  Qed.
End Q6.

314maro

Module Q0_2.
  Theorem tautology : forall P : Prop, P -> P.
  Proof.
    intros P H.
    assumption.
  Qed.
  (*
  Theorem wrong : forall P : Prop, P.
  Proof.
    intros P.

314maro

import Control.Applicative
import Control.Monad.State
import Data.Char

data Op = Add | Sub | Mul | Div | LParens
  deriving (Show)
priority :: Op -> Int
priority Add = 2
priority Sub = 2
priority Mul = 3

314maro

#include <stdio.h>
#include <stdlib.h>
#include <ctype.h>

enum oper { lparens, add, sub, mul, div_op };

int pri(enum oper op) {
  switch (op) {
    case lparens:
      return 0;

314maro

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies, ScopedTypeVariables #-}
import Data.Void
import Data.Bifunctor
import Control.Comonad
import qualified Data.Monoid as M

-- i -> f はよくないかもしれない
class Bifunctor f => Monoidal i f | i -> f, f -> i where
  midL1 :: a -> f i a

314maro

#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <ctype.h>
#include <string.h>
#include <time.h>

// TODO: 値を返すところで NULL のかわりをしたい
typedef long long int_val;

314maro

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
import Data.Monoid
import Control.Applicative

newtype AppMon f m = AppMon { getAppMon :: f m }
  deriving (Functor, Applicative)

instance (Applicative f, Monoid m) => Monoid (AppMon f m) where
  mempty = pure mempty
  mappend = liftA2 mappend

314maro

### ラムダ
🐫 変数👉 式
### 括弧
🌜 式🌛 
### コメント
🌝 コメ🌝 ネストできる🌞 ント🌞 
### 例
🐫 🐭 👉  🐫 🐮 👉  🐫 🐯 👉  🐭 🐯 🌜 🐮 🐯 🌛  🌝 Sコンビネータ🌞 
### バグ
変数まわりにバグがある