krtx

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

{
  "1. Nature": {
    "Weather and landscape symbols": {
      "BLACK SUN WITH RAYS": "☀",
      "CLOUD": "☁",
      "UMBRELLA WITH RAIN DROPS": "☔",
      "SNOWMAN WITHOUT SNOW": "⛄",
      "HIGH VOLTAGE SIGN": "⚡",
      "CYCLONE": "🌀",
      "FOGGY": "🌁",

krtx

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

krtx

#include <Magick++.h>
#include <ncurses.h>
#include <unistd.h>
#include <vector>
#include <algorithm>

int main(int argc, char *argv[])
{

  bool full = false;

krtx

#!/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

require 'pp'

str = 'a+b*c*(d+e)+f+g'

$idx = 0

def term(str)
  ops = []
  while $idx < str.length
    if str[$idx] == '('

krtx

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(' - ')

krtx

;; '((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)))))

krtx

require 'pp'
require 'set'

class Array
  def rotmin
    self.rotate(self.index(self.min))
  end
end

class Permutation < Array

krtx

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