This file contains hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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
(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)) |
This file contains hidden or 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 Ackerman where | |
open import Data.Empty | |
open import Data.Nat | |
open import Relation.Binary.PropositionalEquality | |
open ≡-Reasoning | |
A : ℕ → ℕ → ℕ | |
A _ 0 = 0 |
This file contains hidden or 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 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) |
This file contains hidden or 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 implicationallogic where | |
module Example where | |
postulate | |
Person : Set | |
john : Person | |
mary : Person | |
IsStudent : Person → Set |
This file contains hidden or 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 5f where | |
postulate | |
A : Set | |
B : Set | |
postulate | |
a′ : A | |
b′ : B |