david-christiansen

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

edwinb

module Main
  
{- Divide x by y, as long as there is a proof that y is non-zero. The
   'auto' keyword on the 'p' argument means that when safe_div is called,
   Idris will search for a proof. Either y will be statically known, in
   which case this is easy, otherwise there must be a proof in the context.

   'so : Bool -> Type' is a predicate on booleans which only holds if the
   boolean is true. Essentially, we are making it a requirement in the type
   that a necessary dynamic type is done before we call the function -}

lmarburger

data Expr = Var String
          | Val Int
          | Add Expr Expr
          | Let (List (String, Int)) Expr

data Eval : Type -> Type where
  MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where

yomimono

#!/bin/bash

#set -e
#set -x

fail() {
	echo $1
	[ -e ${EBS_DEVICE} ] && [ "$VOLUME_ID" != "" ] && [ $REGION != "" ] && {
		ec2-detach-volume --region $REGION $VOLUME_ID
		ec2-delete-volume --region $REGION $VOLUME_ID	

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

jlongster

var fs = require('fs');
var path = require('path');
var sweet = require('sweet.js');

module.exports = function(grunt) {
    grunt.initConfig({
        sweetjs: {
            options: {
                modules: ['es6-macros'],
                sourceMap: true,

jvns

Step 0: A program, and prerequisites

We're going to be dealing with a "Hello, world!" program. Just one. There's going to be a bunch of fruit for discussion here. I'm going to be assuming you're on Linux, because we're gonna be talking about ELF and Macs use Mach-O and I don't know anything about Mach-O.

#include <stdio.h>

char *penguin = "Penguin";
char array[5] = {'a', 'b', 'c', 'd', 'e'};

klutzy

// emscripten uses le32-unknown-nacl triple but rustc doesn't know it now.
// So just use similar target instead.
// `rustc hello.rs --target=i686-unknown-linux --emit-llvm -S --cfg libc`
// `emcc hello.ll -o hello.js`

// no `extern mod`.
#[no_std];
#[feature(macro_rules)];

use core::container::Container;

NicolasT

{-# LANGUAGE RebindableSyntax,
             KindSignatures,
             DataKinds,
             GADTs,
             GeneralizedNewtypeDeriving,
             StandaloneDeriving,
             FlexibleInstances,
             Rank2Types #-}

module Connection (

timjb

Hello, my name ist {{name}} and I am {{age}} years old.