Skip to content

Instantly share code, notes, and snippets.

Avatar

Ting-gan LUA banacorn

  • Academia Sinica
  • Taipei, Taiwan
View GitHub Profile
View Bin.agda
module Bin where
-- `Set` is a reserved word in Agda, it's the type of all types
-- We are declaring that `Bin` is of type `Set`, `■` is of type `Bin`, and so on ...
data Bin : Set where
: Bin -- 0
0,_ : Bin Bin -- 2n
1,_ : Bin Bin -- 2n+1
-- Binary number in a reversed order, for example
View 從近期的抗爭談些社會意識的錯誤
批踢踢實業坊›看板 Gossiping
作者Machinator (\⊙▽⊙/)
看板Gossiping
標題[爆卦] 從近期的抗爭談些社會意識的錯誤
時間Mon Apr 14 22:09:04 2014
錯誤一:「警察是無辜的,要找就找後面下令的人。」
複製貼上故事:
View benchmark
# confidence from 0% to 100%
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0 100 +RTS -K2000m -H500m -RTS
4.48 real 3.85 user 0.34 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.1 100 +RTS -K2000m -H500m -RTS
3.96 real 3.59 user 0.32 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.2 100 +RTS -K2000m -H500m -RTS
3.92 real 3.57 user 0.31 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.3 100 +RTS -K2000m -H500m -RTS
3.97 real 3.60 user 0.33 sys
View BatBunker.hs
module BatBunker where
import Data.List (findIndices, delete, (\\))
import Data.Ratio
data Cell = Empty | Wall | Bat | AlphaBat deriving (Show, Eq)
type Map = [[Cell]]
type Coord = (Int, Int)
type Vertex = (Cell, Coord)
View maximum.hs
maximum :: Ord a => [a] -> a
maximum = foldr max (-∞)
View sumWithIOAndST.hs
import Control.Monad (forM_)
import Control.Monad.ST (runST)
import Data.IORef
import Data.STRef
-- dirty, can't get rid of IO
sumIO :: [Int] -> IO Int
sumIO xs = do
acc <- newIORef 0
forM_ xs (modifyIORef acc . (+))
View fuck-final.md

Ring

Chain of class inclusions

Rings ⊃ Commutative rings ⊃ ID ⊃ UFD ⊃ PID ⊃ ED ⊃ Field

Prime

if a | bc then a | b or a | c, i.e. a can't be torn apart if a is prime

View flolac14.md

Semantics

Lecture 1

  • p. 11: For every three terms M0, M1, and M2 => For every three terms M1, M2, and M3

Type Theory & Logic

Lecture 2

@banacorn
banacorn / agda-os-x.md
Last active Aug 29, 2015
Agda Mac OS X 安裝指南
View agda-os-x.md
View budda
_oo0oo_
o8888888o
88" . "88
(| -_- |)
0\ = /0
__/`---'\__
.' \\| |// '.