wires

Require Import Zpower Zpow_facts ZArith NArith.

Open Scope Z_scope.

Lemma Z_powers_add : forall n : Z,
 0 < n -> 2 ^ (n - 1) + 2 ^ (n - 1) = 2 ^ n.
Proof.
 intros.
 replace (2 ^ n) with (2 ^ (1 + (n - 1))) by (f_equal; omega).
 rewrite Zpower_exp; change (2 ^ 1) with 2; omega.

wires

;; local settings for proof general
((coq-mode . (
(coq-prog-args . ("-emacs-U" "-R" "/home/wires/w/HoTT/Coq/" "\"\"")
(coq-prog-name . "/home/wires/opt/coq-trunk-14023-p_coqdoc/tags/V8.3pl1/bin/coqtop")
)))

wires

;;; pretty-mode.el --- redisplay parts of the buffer as pretty symbols
;;; -*- coding: utf-8 -*-

;;; Commentary:
;; 
;; Minor mode for redisplaying parts of the buffer as pretty symbols
;; originally modified from Trent Buck's version at http://paste.lisp.org/display/42335,2/raw
;; Also includes code from `sml-mode'
;; See also http://www.emacswiki.org/cgi-bin/wiki/PrettyLambda
;; 

wires

;;; lambda-mode.el --- Pretty-print lambdas

;; Author: Mark Triggs <mst@dishevelled.net>

;; This file is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 2, or (at your option)
;; any later version.

;; This file is distributed in the hope that it will be useful,

wires

(*

(** Simple streams created by iteration of one operator *)
Section monoid_iter.
  Context `{Monoid M} (m:M).
  
  (** The infinite stream s, m & s, m & m & s, ... *)
  CoFixpoint inf_iter (start:M) : ∞M :=
    start ::: inf_iter (m & start).
  

wires

export ES='http://localhost:9200'


# avoid colorizing when using less
if [ -t 1 ]; then
	alias pp='python -mjson.tool | pygmentize -l javascript'
else
	alias pp='python -mjson.tool'
fi

wires

#! /bin/sh

# I first create the large file, so we are sure this has nothing to do with stream piping
node create_large_file.js > large.json

# on my machine this crashes on 133949
cat large.json | node nothing.js
#....
#133949
#FATAL ERROR: CALL_AND_RETRY_2 Allocation failed - process out of memory

wires

import static java.lang.Math.max;
import static java.lang.Math.min;

public class Math
{
    // clamp(n) = n such that min <= final <= max
    public static final int clamp(final int min, final int value, final int max)
    {
        return max(min, min(value, max));
    }

wires

import android.graphics.Canvas;
import android.graphics.Paint;
import android.graphics.Rect;
import android.graphics.drawable.shapes.Shape;

/**
 * Centered string shape
 */
class StringShape extends Shape
{

wires

import com.google.inject.*;
import org.nnsoft.guice.sli4j.core.InjectLogger;
import org.nnsoft.guice.sli4j.slf4j.Slf4jLoggingModule;
import org.slf4j.Logger;

class Stuff {
    public int randomNumber() {
        return (int)(Math.random() * Integer.MAX_VALUE);
    }
}