krtx

#!/bin/bash

# tmux requires unrecognized OSC sequences to be wrapped with DCS tmux;
# <sequence> ST, and for all ESCs in <sequence> to be replaced with ESC ESC. It
# only accepts ESC backslash for ST.
function print_osc() {
    if [[ -n $TERM ]] ; then
        printf "\033Ptmux;\033\033]"
    else
        printf "\033]"

krtx

module EvalContML1 where

open import Data.Nat as N using (ℕ)
open import Data.Bool as B using (Bool; false; true)
open import Relation.Binary.PropositionalEquality

data Value : Set where
  int : ℕ → Value
  bool : Bool → Value

krtx

module Demo where

open import Relation.Binary.PropositionalEquality

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

infixl 5 _+_
infixl 6 _*_

krtx

package main

import (
	"errors"
	"fmt"
	"math/rand"
	"net"
	"os"
	"os/signal"
	"strconv"

krtx

module Z3 = ZZ3.Make (struct let ctx = Z3.mk_context [] end)

open Z3

let solve board =

  let cells =
    Array.init 9 (fun i ->
      Array.init 9 (fun j ->
        Symbol.declare Int (Printf.sprintf "%d%d" i j)))

krtx

module 5f where

postulate
  A : Set
  B : Set

postulate
  a′ : A
  b′ : B

krtx

module implicationallogic where

module Example where

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

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 Ackerman where

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

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

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