wires

var Q = require('kew');

function retryPromise(n, mkPromise) {
    if(n > 0)
        return mkPromise()
            .fail(function(){
                console.log('failed promise, retrying maximum ' + n + ' more times');
                return retryPromise(n - 1, mkPromise);
            });

wires

/** nigga wut */
background: #366;
background: linear-gradient(25deg, #346, rgba(100,0,100,0.1));
min-height: 100%;

font-family: monospace;
font-size: 48pt;

wires

Keybase proof

I hereby claim:

• I am wires on github.
• I am wires (https://keybase.io/wires) on keybase.
• I have a public key whose fingerprint is 1124 72AA E064 3240 BA03 8B2B 4E2D 3ABE 1D30 C38D

To claim this, I am signing this object:

wires

var http = require('http')

var d = {
    title: 'TblParlement Levend',
    editor: 'Waag Society',
    license: 'CC-BY',
    description: 'Parlement Levend',
    website: 'http://waag.org',
    author: 'Waag',
    id: 'fo'

wires

{"distance_table":[[0,30206,0,36651,0,13279,0,32380,0,12034,0,12283,0,41180,0,20602,0,35271,0,51101,0,45807,0,22371,0,27365,0,40789,40789,30206,40789,36651,40789,13279,40789,32380,1960982,1960982,1960982,1960982],[29170,0,29170,15583,29170,37178,29170,50285,29170,35919,29170,36620,29170,59085,29170,38507,29170,21171,29170,69006,29170,63712,29170,26939,29170,45902,29170,25115,25115,0,25115,15583,25115,37178,25115,50285,1942829,1942829,1942829,1942829],[0,30206,0,36651,0,13279,0,32380,0,12034,0,12283,0,41180,0,20602,0,35271,0,51101,0,45807,0,22371,0,27365,0,40789,40789,30206,40789,36651,40789,13279,40789,32380,1960982,1960982,1960982,1960982],[36468,15986,36468,0,36468,31574,36468,55820,36468,30853,36468,39965,36468,66946,36468,46368,36468,12548,36468,76867,36468,71573,36468,21335,36468,50326,36468,11309,11309,15986,11309,0,11309,31574,11309,55820,1932678,1932678,1932678,1932678],[0,30206,0,36651,0,13279,0,32380,0,12034,0,12283,0,41180,0,20602,0,35271,0,51101,0,45807,0,22371,0,27365,0,40789,40789,30206,40789,36

wires

Require Import 
  additional_operations.

Check (1^3).
(* 1 ^ 3
     : nat *)

Require Import Streams.

Notation "∅ x" := (Stream x) (at level 38).

wires

Section s1.
Context `{Ring R}. (* Error: Unbound and ungeneralizable variable Ring *)
(* That's a clear error message *)
End s1.

Require Import canonical_names.
Section s2.
Context `{Ring R}. (* Error: Cannot infer the type of R. *)
(* it haz confusing, why happens? *)

wires

(* http://coq.inria.fr/stdlib/Coq.Bool.Bvector.html

   Section VECTORS --> Vcons, Vextend   -- this I cannot use?
   Section BOOLEAN_VECTORS --> Bcons    -- this I can use
*)

Require Import Bvector.

Check (Bcons).

wires

Require Import Utf8 String ZArith.

(* IO is done through this JSON inductive type *)
Inductive JSON :=
  | JObject : list (string * JSON) → JSON
  | JArray : list JSON → JSON
  | JString : string → JSON
  | JNumber : Z → JSON
  | JBool : bool → JSON
  | JNull : JSON.

wires

Infix "×" := prod (at level 60).

Coercion bool_in_nat := fun b:bool => if b then 0 else 1.

Definition a : nat := false.

Definition foo (p:bool × bool) : bool × nat :=
  (fst p, snd p:nat).

Coercion fooc := foo.