yanok

val wc = Wildcard
val x = Variable "x"
val y = Variable "y"
val z = Variable "z"

fun tpl vs = Tuple vs
fun pair (a,b) = Tuple [a,b]
fun tp ps = TupleP ps
fun pp (a,b) = TupleP [a,b]

yanok

.intel_syntax

.section .rodata
    main.S_0:
        .string	"Hello, world!\n"
.text
        .global	main
        .type	main,	@function
    main:
        push %rbp

yanok

#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

typedef struct{ long _size; void* _data; } _ArrayHandle;
typedef void _RecordHandle;

/* -------- intrinsics -------- */
char* append(char* lhs, char* rhs) {

yanok

.intel_syntax
/* main : () -> int */
.text
    .globl _main
  _main:
    push    rbp
    mov     rbp, rsp
    lea     rdi, [rip + main.S_0]
    call    _print
  main.L_main0:

yanok

------------------------------------------------------
------------------------------------------------------
------------------ Crash Log Begin -------------------


Current System time: "2013-06-23 12:06:57"
Build version: 9.6.2.209584
Build configuration: Product--ARCHFAM
OS version: 5.0

yanok

module DataStore

import Data.Vect

infixr 5 .+.

public export
data Schema = SString | SInt | (.+.) Schema Schema

%name Schema sch, sch1

yanok

import Data.Vect

data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkWordState : (word : String) ->
                   (missing : Vect letters Char) ->
                   WordState guesses_remaining letters

data Finished : Type where
     Lost : (game : WordState 0 (S letters)) -> Finished
     Won : (game : WordState (S guesses) 0) -> Finished

yanok

data InfIO : Type where
     Do : IO a ->
          (a -> Inf InfIO) ->
          InfIO

total
run : InfIO -> IO ()
run (Do x f) = do r <- x
                  run (f r)

yanok

POST /favorites 413 0.816 ms - 2694
PayloadTooLargeError: request entity too large
    at readStream (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/raw-body/index.js:155:17)
    at getRawBody (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/raw-body/index.js:108:12)
    at read (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/body-parser/lib/read.js:77:3)
    at jsonParser (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/body-parser/lib/types/json.js:134:5)
    at Layer.handle [as handle_request] (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/express/lib/router/layer.js:95:5)
    at trim_prefix (/Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/solution/node_modules/express/lib/router/index.js:317:13)
    at /Users/ilya/git/git-school/wa/exercises/8-AJAX+WebSockets_Exercises/soluti

yanok

module TraversableVec where

id : forall {k}{X : Set k} -> X -> X
id x = x

_o_ : forall {i j k}
      {A : Set i}{B : A -> Set j}{C : (a : A) -> B a -> Set k} ->
      (f : {a : A}(b : B a) -> C a b) ->
      (g : (a : A) -> B a) ->
      (a : A) -> C a (g a)