This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
"1. Nature": { | |
"Weather and landscape symbols": { | |
"BLACK SUN WITH RAYS": "☀", | |
"CLOUD": "☁", | |
"UMBRELLA WITH RAIN DROPS": "☔", | |
"SNOWMAN WITHOUT SNOW": "⛄", | |
"HIGH VOLTAGE SIGN": "⚡", | |
"CYCLONE": "🌀", | |
"FOGGY": "🌁", |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <Magick++.h> | |
#include <ncurses.h> | |
#include <unistd.h> | |
#include <vector> | |
#include <algorithm> | |
int main(int argc, char *argv[]) | |
{ | |
bool full = false; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
require 'pp' | |
str = 'a+b*c*(d+e)+f+g' | |
$idx = 0 | |
def term(str) | |
ops = [] | |
while $idx < str.length | |
if str[$idx] == '(' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
require 'mp3info' | |
dir = '/my/music/library/' | |
Dir::glob(dir + '*.mp3').each {|f| | |
Mp3Info.open(f) do |mp3| | |
t = mp3.tag.title | |
title = t.slice(t.rindex('/') + 2, t.length) | |
artist = t.slice(0, t.rindex('/') - 1) | |
if title.index(' - ') |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; '((1 . 2) (2 . 3) (3 . 1)) | |
;; '((1 . 4) (2 . 3) (4 . 1) (3 . 2)) | |
;; '((5 . 1) (4 . 2) (2 . 5) (3 . 4) (1 . 3)) | |
(defun mapping (item g) | |
(cdr (assoc item g))) | |
(defun normalize (g) | |
(sort g #'(lambda (x y) (< (car x) (car y))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
require 'pp' | |
require 'set' | |
class Array | |
def rotmin | |
self.rotate(self.index(self.min)) | |
end | |
end | |
class Permutation < Array |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
291 126 -1 | |
269 60 1 | |
293 291 1 | |
265 195 1 | |
380 133 -1 | |
294 211 1 | |
170 156 -1 | |
180 249 1 | |
239 201 1 | |
293 164 -1 |