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

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

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

  bool full = false;

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

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

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

(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

module Ackerman where

open import Data.Empty
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

A : ℕ → ℕ → ℕ
A _       0       = 0

krtx

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)

krtx

module implicationallogic where

module Example where

  postulate
    Person        : Set
    john          : Person
    mary          : Person
    IsStudent     : Person → Set

krtx

module 5f where

postulate
  A : Set
  B : Set

postulate
  a′ : A
  b′ : B