aymanosman

#lang pie

;; Prelude

(claim +
  (-> Nat Nat Nat))
(define +
  (lambda (n m)
    (rec-Nat n
      m

aymanosman

#lang pie

;; Exercises on ind-Nat from Chapter 10 of The Little Typer


;; Prelude

(claim +
  (-> Nat Nat Nat))
(define +

aymanosman

#lang pie

;; Exercises on Nat equality from Chapter 8 and 9 of The Little Typer

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (n m)

aymanosman

#lang pie

;; Exercises on Pi types and using the List elimiator from Chapters 4 and 5
;; of The Little Typer
;;
;; Some exercises are adapted from assignments at Indiana University

(claim elim-Pair
  (Π ((A U)
      (D U)

aymanosman

#lang pie

(claim >
  (-> Nat Nat Nat))
(define >
  (lambda (n)
    (rec-Nat n
      (the (-> Nat Nat) (lambda (m) 0))
      (lambda (n-1 n-1>)
        (lambda (m)

aymanosman

(defn f
  ([xs] (if (empty? xs) () (f (first xs) (rest xs))))
  ([x xs]
   (cond
     (empty? xs) (list x)

     :else
     (let [y (first xs)]
       (cond
         (= x y)

aymanosman

HC      = ghc
HC_OPTS = -cpp $(EXTRA_HC_OPTS)

SRCS = Main.lhs Foo.lhs Bar.lhs
OBJS = Main.o   Foo.o   Bar.o

.SUFFIXES : .o .hs .hi .lhs .hc .s

cool_pgm : $(OBJS)
        rm -f $@

aymanosman

# Sexp equivalent, modulo infix arithmetic expression
# (defmodule M
#   (def foo (lol)
#    2+lol))

# Starting from the "true", most verbose form and applying syntactic rules to
# obtain the final form

# "true" expression, notice there are no vararg functions
defmodule(M,

aymanosman

m = require('mongojs')
J = require('joi')

x = J.string().hex().length(24)
i = m.ObjectId().toString()
// '57a1c20202ccc41cd8d84834'

x.validate(i)
// { error: null, value: '57a1c20202ccc41cd8d84834' }

aymanosman

import Dict exposing (Dict)
import Html exposing (..)
import Html.Attributes exposing (..)
import Html.Events exposing (..)
import String
import Debug exposing (log)
import Json.Decode as Json
import Signal exposing (Address)
import StartApp.Simple
import Json.Decode as Json