eligrey

/*
 * object.watch polyfill
 *
 * 2012-04-03
 *
 * By Eli Grey, http://eligrey.com
 * Public Domain.
 * NO WARRANTY EXPRESSED OR IMPLIED. USE AT YOUR OWN RISK.
 */

ikedaisuke

{-# OPTIONS --universe-polymorphism #-}
module ReverseReverseId where

open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality 
  as P using (_≡_; refl; cong)

ReverseReverseId : ∀ {a} {A : Set a} (xs : List A) -> 
                   reverse (reverse xs) ≡ xs

zziuni

# source : http://code.google.com/p/natvpn/source/browse/trunk/stun_server_list
# A list of available STUN server.

stun.l.google.com:19302
stun1.l.google.com:19302
stun2.l.google.com:19302
stun3.l.google.com:19302
stun4.l.google.com:19302
stun01.sipphone.com
stun.ekiga.net

t0yv0

Require Import Utf8.

Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.

Infix ":>" := subtype (at level 50).

Definition st {x y} f := ST x y f.

Definition unpack {a b : Set} (st : a :> b) :=

twanvl

module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction

gallais

module Sorting where

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary

gbluma

#lang typed/racket

;; We get exhaustive pattern matching

(: f ((U String Integer) -> Boolean))
(define (f x)
  (cond 
    [(string? x) (string=? x "hi")]           ; covers string needs
    [(exact-nonnegative-integer? x) (= x 7)]  ; covers positive integers
    [(even? x) (= x -8)]                      ; we can actually cover a subset of negative integers

chaitanyagupta

Reader Macros in Common Lisp

This post also appears on lisper.in.

Reader macros are perhaps not as famous as ordinary macros. While macros are a great way to create your own DSL, reader macros provide even greater flexibility by allowing you to create entirely new syntax on top of Lisp.

Paul Graham explains them very well in [On Lisp][] (Chapter 17, Read-Macros):

The three big moments in a Lisp expression's life are read-time, compile-time, and runtime. Functions are in control at runtime. Macros give us a chance to perform transformations on programs at compile-time. ...read-macros... do their work at read-time.

kseo

#! /usr/bin/env ocamlscript
Ocaml.ocamlflags := ["-thread"];
Ocaml.packs := [ "core" ]
--
open Core.Std

type term =
  | Ident of string
  | Lambda of string * term
  | Apply of term * term

emallson

;;; nodejs-repl-eval.el --- Summary
;;; Commentary:
;;;
;;; Evaluation functions for the `nodejs-repl' package.  Written on a stormy
;;; night between days of node hacking.
;;; 
;;; Code:

(require 'js2-mode)
(require 'nodejs-repl)