ayu-mushi

Require Import ssreflect.
Section Coq1.
  Variable P Q R : Prop.
  Theorem imp_trans : (P -> Q) -> (Q -> R) -> P -> R.
  Proof.
    intros p q r.
    apply q.
    apply p.
    assumption.
  Qed.

ayu-mushi

var request = require('request');

url = 'https://query.wikidata.org/sparql'

var query="SELECT\
  ?countriesLabel ?countriesDescription ?capitalLabel ?capitalDescription ?inception ?abolished ?dummy\
WHERE {\
  {?countries rdfs:label \"" + process.argv[2] +
  "\"@ja; wdt:P31 wd:Q3624078}\
  UNION {?countries skos:altLabel \"" + process.argv[2] +

ayu-mushi

MAILTO="[email protected]"
SHELL=/bin/zsh
PATH=/usr/local/lib/anaconda2/bin/:/opt/mozart/bin/:/usr/local/ghc-7.10/bin:/usr/local/ghc-7.8.4/bin:/usr/local/ghc-7.10.2/bin/:/usr/local/bin:~/.local/bin:/opt/local/bin:/usr/local/ghc-7.8/bin:~/.cabal/bin/:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/bin/

HOME=/home/ayu-mushi
LANG=ja_JP.UTF-8
LC_ALL=ja_JP.UTF-8
CONTENT_TYPE=text/plain; charset=UTF-8

ayu-mushi

import Control.Monad
import Control.Applicative


-- filterM (const [True, False])

-- filterM :: (Applicative m) => (a -> m Bool) -> [a] -> m [a]
-- filterM p = foldr (\x -> liftA2 (\flg -> if flg then (x:) else id) (p x)) (pure [])

-- (<*>) :: [a -> b] -> [a] -> [b]

ayu-mushi

{-# LANGUAGE JavaScriptFFI      #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuasiQuotes     #-}
{-# LANGUAGE GADTs  #-}
{-# LANGUAGE RecursiveDo  #-}
{-# LANGUAGE ScopedTypeVariables  #-}

module Lib
    ( myMain

ayu-mushi

#!/usr/bin/env python3
# -*- coding: utf-8 -*-

# printenvを使ってw3mでページ毎にコメントを記録できるようにする
# 今まで作ったURLと注釈ファイル名(タイトル、ダブったら数字を付ける)の組の列をjsonで保持 連想配列
# URLを渡すと注釈ファイルが開く
# keymap A EXEC_SHELL "w3m_commentary.py"

import lxml.html
import json

ayu-mushi

『型システム入門――プログラミング言語と型の理論(TaPL)』読書ノート

TaPLを買ったので、誤解があった場合に指摘を受けたりできるように、読書ノートを公開します。 暇な人は間違いを見つけたら教えて下さい。

(このノートの目的上、自信が無いことも言っているので、このノートに書いてあることはあまり信じないように)

###序文

必要な背景知識

ayu-mushi

#!/usr/bin/python

from tika import parser
import argparse
import os
import sys

def print_title(parsed, filename):
    try:
        print(parsed['metadata']['title'])

ayu-mushi

{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving #-}

import Haste
import Haste.Foreign
import Control.Monad.Operational
import Control.Monad.IO.Class
import Control.Applicative

data SleepableIOF a where
  Sleep :: Int -> SleepableIOF ()

ayu-mushi

{-# LANGUAGE DeriveFunctor, FlexibleContexts, UndecidableInstances #-}
import Control.Monad.Free
import Control.Monad (void)
import Control.Monad.Identity
import Data.Void

import Test.QuickCheck

-- Free Monadの使用例