TakashiHarada

;; .emacs

;; for Haskell
(add-hook 'haskell-mode-hook 'haskell-indentation-mode)

;;; uncomment this line to disable loading of "default.el" at startup
;; (setq inhibit-default-init t)

;; enable visual feedback on selections
;(setq transient-mark-mode t)

TakashiHarada

神奈川大学圏論勉強会

メンバー

• 木下修司
• 原田崇司
• 竹視道覚

第2回 2015.04.22.

やったこと

• MacLane P.8の下から2つ目のパラグラフの記述。なぜIdentityが一意に決まるのか？証明できる？

TakashiHarada

module AgdaBasics where

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

TakashiHarada

module Views where

open import Data.Nat renaming (ℕ to Nat)
--open import AgdaBasics

data Parity : Nat → Set where
  even : (k : Nat) → Parity (k * 2)
  odd  : (k : Nat) → Parity (1 + k * 2)

-- zero  + m = m

TakashiHarada

import Data.Char
import System.IO
import System.Random
import System.Environment

numListToString :: [Int] -> String
numListToString []     = []
numListToString (x:xs) = (show x) ++ "\n" ++ numListToString xs

main = do

TakashiHarada

#include <bits/stdc++.h>

using namespace std;

void f(vector<int> *p)
{
	vector<int>::iterator it = p->begin();
	int i = 0;
	int max = 0;
	while (i < p->size())

TakashiHarada

#include <bits/stdc++.h>

using namespace std;

void f(vector<int> *v)
{
	vector<int>::iterator vit, vit_end;
	vector<int>::iterator vit2, vit2_end;
	vit = v->begin();
	int i = 0;

TakashiHarada

#include <bits/stdc++.h>
using namespace std;
#include <stdio.h>
#include <sys/time.h>
#include <sys/resource.h>
#include <sys/types.h>
#include <stdlib.h>
#include <unistd.h>

#define MAX_STRING 128

TakashiHarada

module Universes where

data False : Set where
record True : Set where

data Bool : Set where
  true  : Bool
  false : Bool

isTrue : Bool -> Set

TakashiHarada

makeBitString :: Int -> [String]
makeBitString 0 = []
makeBitString 1 = ["0","1"]
makeBitString w = map ('0':) (makeBitString (w-1)) ++ map ('1':) (makeBitString (w-1))

makeMaskZeroString :: Int -> [String]
makeMaskZeroString w = ((map oneToMask) . makeBitString) w
  where
    oneToMask :: String -> String
    oneToMask = (map (\c -> if c == '1' then '*' else c))