Skip to content

Instantly share code, notes, and snippets.

s.murayama yuga

Block or report user

Report or block yuga

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@yuga
yuga / printf.idr
Created May 17, 2014
skills matterにVideoがあがっていたIdrisで書く型安全なprintf; youtube => http://youtu.be/fVBck2Zngjo
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
@yuga
yuga / andb_false.v
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.
@yuga
yuga / typeclass0.hs
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
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)
@yuga
yuga / cow.bash
Created Aug 12, 2014
cowbuilderのバッドノウハウ集
View cow.bash
#!/bin/bash
PRG=$(readlink -f "$0")
PRGDIR=$(dirname "${PRG}")
set -x
set -e
list=(
haskell-names-th_0.0.1.0.dsc
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]
@yuga
yuga / decimal.idr
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
@yuga
yuga / gist:328a5bdf885f1599d28d
Created Dec 11, 2014
SQLite3用のモジュール名をどれにあわせるか?
View gist:328a5bdf885f1599d28d
HSQL
--------------------
DB.HSQL.SQLite3
HDBC
--------------------
Database.HDBC.Sqlite3
HDBI
--------------------
@yuga
yuga / exmaples.hs
Last active Aug 29, 2015
追加しようと思うexample
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
You can’t perform that action at this time.