sunaemon

vim.cmd [[autocmd BufWritePost plugins.lua PackerCompile]]
require('plugins')

vim.cmd [[filetype plugin indent on]]
vim.cmd [[syntax enable]]

-- display setting
vim.o.list = true -- show tab trail etc...
vim.o.listchars = 'tab:» ,trail:_,extends:>,precedes:<' -- specify how them displayed
vim.o.wildmode = 'list:full'

sunaemon

$ satysfi --show-fonts hello.saty
 ---- ---- ---- ----
  target file: 'hello.pdf'
  dump file: 'hello.satysfi-aux' (already exists)
  parsing 'hello.saty' ...
  parsing 'stdjareport.satyh' ...
  parsing 'pervasives.satyh' ...
  parsing 'gr.satyh' ...
  parsing 'geom.satyh' ...
  parsing 'list.satyg' ...

sunaemon

#include <stdio.h>
#include <vector>
#include <time.h>

using namespace std;

void fun1(int *x, int n)
{
    for (int i = 1; i<= n; i++)
        x[i] += x[i - 1];

sunaemon

#!/usr/bin/env python3

# License: MIT
# http://qiita.com/sunaemon0/items/d45fe7040d8007801b88

import argparse
import re
import sys

parser = argparse.ArgumentParser(description='merge')

sunaemon

FROM debian:wheezy

# install packages
ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update && apt-get upgrade -y

#install tools for logging and process administration
RUN apt-get install -y monit rsyslog
WORKDIR /
RUN apt-get install -y ruby ruby-dev build-essential wget

sunaemon

#include <sys/select.h>
#include <fcntl.h>
#include <stdio.h>
int main()
{
    int sock = open("/dev/urandom", O_RDONLY);
    int r;
    fd_set rfds;
    FD_ZERO(&rfds);
    FD_SET(sock, &rfds);

sunaemon

FROM debian:wheezy

MAINTAINER sunaemon <@sunaemon0>

# install packages
RUN echo 'Acquire::http { Proxy "http://hogehoge:3142"; }; ' > /etc/apt/apt.conf.d/50-apt-cacker.conf
ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update && apt-get upgrade -y

#install tools for logging and process administration

sunaemon

Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
Require Import Classical. 
intros; tauto.
Qed.

Goal
  forall P Q R : Prop,

sunaemon

Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  refine (fun P Q R H => _).
  refine (match H with
              | or_introl HP => _
              | or_intror  HnQR => _
          end).
  - exact (conj (or_introl HP) (or_introl HP)).
  - refine (conj _ _).
    + refine (or_intror (fun HQ => _)).

sunaemon

Parameter A : Set.
 
Definition Eq := fun a b:A => forall ee : A->A->Prop, ee a a -> ee a b.
 
Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros x y.
unfold Eq.
split.
+ intro H.