ryuta-ito

if !exists("*Re()")
  function! Re()
    source $MYVIMRC
  endfunction
  command! Re call Re()
endif

if !exists("*Ed()")
  function! Ed()
    source $MYVIMRC

ryuta-ito

Require Import Relation_Definitions.

Arguments reflexive A/.
Arguments transitive A/.
Arguments symmetric A/.
Arguments antisymmetric A/.

Section FinSemiLattice.
  Variable X : Type.

ryuta-ito

[1] pry(main)> Sequent.build('∀x.(P(x) => Q(x)) |- ∀x.(P(x) ∧ R(x) => Q(x) ∧ R(x))').show_lk_proof_figure
P(A) |- P(A)
------ (W R)
P(A) |- Q(A), P(A)
------ (W L)
P(A), R(A) |- Q(A), P(A)
------ (W L)
∀x.(P(x) => Q(x)), P(A), R(A) |- Q(A), P(A)
    Q(A) |- Q(A)

ryuta-ito

diff --git a/config/application.rb b/config/application.rb
index 282a956..3aa17b2 100644
--- a/config/application.rb
+++ b/config/application.rb
@@ -16,6 +16,10 @@ module Sample
     # -- all .rb files in that directory are automatically loaded after loading
     # the framework and any gems in your application.
     config.i18n.default_locale = :ja
+    config.generators do |g|
+      g.javascript_engine :coffee

ryuta-ito

class Hoge < ApplicationRecord
  before_save :arrange_bed_number

  def self.bed_numbers
    {
      bed_number_1: 1,
      bed_number_2: 2,
      bed_number_3: 4,
    }

ryuta-ito

halt(x, y): xにyを適用した際に
  | 停止する場合 -> True
  | 無限ループする場合 -> False

X(x): halt(x, x)が
  | Trueの場合 -> 無限ループをする
  | Falseの場合 -> Trueを返す(停止する)

X(x)の指標をeしたとき

ryuta-ito

import org.apache.poi.ss.usermodel.*;
import org.apache.poi.ss.formula.*;
import org.apache.poi.ss.formula.ptg.*;
import org.apache.poi.xssf.usermodel.*;
import org.apache.poi.ss.util.CellReference;
import java.io.*;
import org.apache.poi.openxml4j.exceptions.*;

public class PoiExample {
    public static void main(String[] args) {

ryuta-ito

条件で絞り込んだテーブルとのright outer join & includes

class Bill
  def self.with_company(bill_month)
    joins(sanitize_sql_array(['right outer join companies on companies.id = bills.company_id and bills.bill_month = ?', bill_month])).select('bills.*, companies.id as company_id').includes(:user)
  end
end

ryuta-ito

Require Import Image.

Arguments Im {U V}.
Arguments In {U}.
Arguments Included {U}.

Section InvImage.

Variables U V : Type.

ryuta-ito

• pattern
  • \%<num>l: 行全体
• \%c: 列全体