[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)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
if !exists("*Re()") | |
function! Re() | |
source $MYVIMRC | |
endfunction | |
command! Re call Re() | |
endif | |
if !exists("*Ed()") | |
function! Ed() | |
source $MYVIMRC |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Relation_Definitions. | |
Arguments reflexive A/. | |
Arguments transitive A/. | |
Arguments symmetric A/. | |
Arguments antisymmetric A/. | |
Section FinSemiLattice. | |
Variable X : Type. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
class Hoge < ApplicationRecord
before_save :arrange_bed_number
def self.bed_numbers
{
bed_number_1: 1,
bed_number_2: 2,
bed_number_3: 4,
}
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
halt(x, y): xにyを適用した際に | |
| 停止する場合 -> True | |
| 無限ループする場合 -> False | |
X(x): halt(x, x)が | |
| Trueの場合 -> 無限ループをする | |
| Falseの場合 -> Trueを返す(停止する) | |
X(x)の指標をeしたとき |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Image. | |
Arguments Im {U V}. | |
Arguments In {U}. | |
Arguments Included {U}. | |
Section InvImage. | |
Variables U V : Type. |
- pattern
\%<num>l
: 行全体
\%c
: 列全体
NewerOlder