Skip to content

Instantly share code, notes, and snippets.

@krtx
krtx / catagif.rb
Last active December 19, 2015 10:49
animation gif player on terminal
#!/usr/bin/env ruby
require 'curses'
require 'RMagick'
Curses.noecho
Curses.init_screen
Curses.stdscr.keypad(true)
Curses.start_color
Curses.timeout = 0 # non-blocking getch
@krtx
krtx / agif.cpp
Last active December 19, 2015 19:38
animation gif player 256 colors version
#include <Magick++.h>
#include <ncurses.h>
#include <unistd.h>
#include <vector>
#include <algorithm>
int main(int argc, char *argv[])
{
bool full = false;
@krtx
krtx / snum.ml
Created March 16, 2014 06:55
surreal number implementation from On Numbers and Games
type snum = snums * snums
and snums = Nil | Cons of (snum * snums)
let zero = (Nil, Nil)
let one = (Cons (zero, Nil), Nil)
let mone = (Nil, Cons (zero, Nil))
let half = (Cons (zero, Nil), Cons (one, Nil))
let two = (Cons (one, Nil), Nil)
let rec map f = function
{
"1. Nature": {
"Weather and landscape symbols": {
"BLACK SUN WITH RAYS": "☀",
"CLOUD": "☁",
"UMBRELLA WITH RAIN DROPS": "☔",
"SNOWMAN WITHOUT SNOW": "⛄",
"HIGH VOLTAGE SIGN": "⚡",
"CYCLONE": "🌀",
"FOGGY": "🌁",
@krtx
krtx / Bisim.agda
Last active August 29, 2015 14:07
strong bisimulation is equivalence
module Bisim where
open import Data.Nat
open import Data.List
open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
@krtx
krtx / test-ex1.3.scm
Created October 20, 2014 01:28
test for ex 1.3
(use gauche.test)
(test-start "test")
;; insert here
(define target PROGRAM-NAME)
(define (right a b c)
(let ((l (sort (list a b c) >)))
(let ((x (list-ref l 0))
@krtx
krtx / Ackerman.agda
Created November 3, 2014 02:45
SICP Exercise 1.10.
module Ackerman where
open import Data.Empty
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
A : ℕ → ℕ → ℕ
A _ 0 = 0
@krtx
krtx / classic.agda
Last active August 29, 2015 14:10
classical logic
module classic where
open import Level
open import Relation.Nullary
open import Data.Empty
open import Data.Sum
open import Data.Product
-- peirce : ∀ {a b} (P : Set a) (Q : Set b) → Set (a ⊔ b)
module implicationallogic where
module Example where
postulate
Person : Set
john : Person
mary : Person
IsStudent : Person → Set
@krtx
krtx / 5f.agda
Last active October 26, 2015 08:28
module 5f where
postulate
A : Set
B : Set
postulate
a′ : A
b′ : B