{{ message }}

Instantly share code, notes, and snippets.

# s.murayama yuga

Created May 17, 2014
View printf.idr
 module Printf %default total data Format = FInt Format -- %d | FString Format -- %s | FOther Char Format -- [a-zA-Z0-9] | FEnd -- format : List Char -> Format
Last active Aug 29, 2015
Logic_J.vより抜粋。tacticを使わずに証明オブジェクトを手書きするのを試しているけど僕には難しい。
View andb_false.v
 (* **** Exercise: 1 star (bool_prop) *) (** **** 練習問題: ★ (bool_prop) *) Theorem andb_false : forall b c, andb b c = false -> b = false \/ c = false. Proof. intros b c H. unfold andb in H. destruct b. right. apply H. left. reflexivity.
Created Jun 27, 2014
typeclass0.hs の例でのコンパイルエラーを前に少し悩んだので。
View typeclass0.hs
 class Producer p where get :: Resource r => p -> r class Resource a where fire :: a -> Int data A = A Int data B = B Int instance Producer A where
Last active Aug 29, 2015
View Logic_five_not_even.v
 Definition five_not_even' : ~ ev 5 := fun (Hev5 : ev 5) => (fun (P : nat -> Prop) (* evの帰納法の原理*) (f : P 0) (f0 : forall n : nat, ev n -> P n -> P (S (S n))) => fix F (n : nat) (e : ev n) {struct e} : P n := (* eについて減少 *) match e in (ev n0) return (P n0) with | ev_0 => f | ev_SS n1 ev1 => f0 n1 ev1 (F n1 ev1) end)
Created Aug 12, 2014
cowbuilderのバッドノウハウ集
View cow.bash
Last active Aug 29, 2015
View ChunkGroupBy.hs
 -- > chunkGroupBy (\x y -> x == y) 6 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3] -- [[[0,0,0,0]],[[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]] -- -- > chunkGroupBy (\x y -> x == y) 7 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3] -- [[[0,0,0,0],[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]] -- -- > chunkGroupBy (\x y -> x == y) 15 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3] -- [[[0,0,0,0],[1,1,1],[2,2,2,2,2]],[[3,3,3,3]]] -- -- > chunkGroupBy (\x y -> x == y) 16 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
Last active Aug 29, 2015
not deal with seriously
View decimal.idr
 module decimal record Decimal : Nat -> Type where MkDecimal : (places : Nat) -> (mantissa : Integer) -> Decimal places signum : Integer -> Integer signum n = case compare n 0 of LT => (-1) EQ => 0 GT => 1
Created Dec 11, 2014
SQLite3用のモジュール名をどれにあわせるか？
View gist:328a5bdf885f1599d28d
 HSQL -------------------- DB.HSQL.SQLite3 HDBC -------------------- Database.HDBC.Sqlite3 HDBI --------------------
Last active Aug 29, 2015

View exmaples.hs
 account1'' :: Relation () Account1 account1'' = relation \$ do a <- query account wheres \$ a ! Account.productCd' `in'` values ["CHK", "SAV", "CD", "MM"] return \$ Account1 |\$| a ! Account.accountId' |*| a ! Account.productCd' |*| a ! Account.custId' |*| a ! Account.availBalance' data Account1 = Account1
Last active Aug 29, 2015
SQL: date time literals