Skip to content

Instantly share code, notes, and snippets.

View fluiddynamics's full-sized avatar

fluiddynamics

0 followers · 3 following
View GitHub Profile
@fluiddynamics
fluiddynamics / ランチ.txt
Last active September 29, 2019 03:04
菜香苑 銀座店
営業時間 日曜 11:00～14:30 16:30〜22:30
03-6264-3677
https://tabelog.com/tokyo/A1301/A130101/13196246/
ヴォメロ (Vomero)
営業時間 日曜 11:30～22:00
050-5869-5049
https://tabelog.com/tokyo/A1301/A130101/13139857/
@fluiddynamics
fluiddynamics / Subtyping_J.v
Last active January 8, 2018 13:50
(** * Subtyping_J :サブタイプ *)
(* * Subtyping *)
(* $Date: 2011-05-07 21:28:52 -0400 (Sat, 07 May 2011) $ *)
Require Export MoreStlc_J.
(* ###################################################### *)
(* * Concepts *)
(** * 概念 *)
@fluiddynamics
fluiddynamics / division.v
Created May 6, 2017 11:49
Require Export Coq.Init.Nat.
Print div.
Print modulo.
Print nat.
Print divmod.
Eval compute in (divmod 11 2 1 10).
@fluiddynamics
fluiddynamics / gist:cf094a31e671a789515bcdd81753916f
Last active April 20, 2017 21:01
Java syntax
/*
http://docs.oracle.com/javase/specs/jls/se8/html/jls-19.html
  http://www.bottlecaps.de/rr/ui
*/
ClassDeclaration ::= NormalClassDeclaration | EnumDeclaration
NormalClassDeclaration ::= ClassModifier* 'class' Identifier TypeParameters? Superclass? Superinterfaces? ClassBody
ClassModifier ::= Annotation | 'public' |'protected' | 'private' | 'abstract' | 'static' | 'final' | 'strictfp'
@fluiddynamics
fluiddynamics / coq.ipynb
Created October 5, 2016 21:52
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@fluiddynamics
fluiddynamics / README.md
Last active October 1, 2016 09:52
Hello bl.ocks
@fluiddynamics
fluiddynamics / Ltac.ipynb
Last active September 21, 2016 07:42
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@fluiddynamics
fluiddynamics / DefaultKeyBinding.dict
Created August 17, 2016 18:05
{
"~c" = ( "insertText:", "→" );
"~C" = ( "insertText:", "⇒" );
"~g" = ( "insertText:", "γ" );
"~G" = ( "insertText:", "Γ" );
"~o" = ( "insertText:", "⊥" );
"~O" = ( "insertText:", "⊤" );
"~d" = ( "insertText:", "⊃" );
"~s" = ( "insertText:", "⊂" );
"~S" = ( "insertText:", "∈" );
@fluiddynamics
fluiddynamics / dependent.v
Last active August 16, 2016 07:46
Variable A:Set.
Inductive Vec : nat -> Set:=
| VNil : Vec 0
| VCons : forall n, A -> Vec n -> Vec (S n).
Print Vec.
Inductive bool := | true | false.
@fluiddynamics
fluiddynamics / casebool.v
Last active August 16, 2016 01:32
Inductive bool : Type := |true | false.
Inductive eq A x : A -> Prop := eq_refl : eq A x x.
Inductive or A B : Prop:=
| or_introl : A -> or A B
| or_intror : B -> or A B.
Definition case_bool x : or (eq bool x true) (eq bool x false) :=
match x with