kidoman

#include <stdlib.h>
#include <stdio.h>
#include <math.h>

typedef int i;       //Save space by using 'i' instead of 'int'
typedef float f;     //Save even more space by using 'f' instead of 'float'

//Define a vector class with constructor and operator: 'v'
struct v {
  f x,y,z;  // Vector has three float attributes.

cnd

use std::task;
use std::rt::io::timer::sleep;

///<Summary>
///Simple butterfly
///</Summary>
pub fn butterfly<U>(f: &fn() -> U) -> U { 
    let (port, chan) = stream();
    do task::spawn_sched(task::SingleThreaded) {
        print(" ");

gelisam

-- in reply to http://www.reddit.com/r/haskell/comments/23uzpg/lens_is_unidiomatic_haskell/
-- 
-- What the lens library might look like if Getter, Setter, Fold, Traversal,
-- Lens, Review, and Prism were separate datatypes.
-- 
-- For each optic, I only define enough combinators to explore pairs/sums
-- and lists of integers. Whenever possible, I reimplement the same
-- combinators and the same examples with all optics.

module IdiomaticLens where

rntz

(* A quick note about preorders; skip this if you know about them.
 *
 * A preorder is a relation (a ≤ b) satisfying two rules:
 * 1. Reflexivity: a ≤ a.
 * 2. Transitivity: if a ≤ b and b ≤ c then a ≤ c.
 *
 * A good example of a preorder is "lists under containment":
 * let (X ≤ Y) if every element of the list X is also in Y.
 *
 * Preorders are like partial orders, but without requiring antisymmetry.

ichistmeinname

Require Import Lists.List.
Require Import Arith.Arith.

Require Import Omega.

Set Implicit Arguments.

Fixpoint replicate A (n : nat) (x : A) : list A :=
  match n with
  | O => nil

UlfNorell

-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown.
-- https://www.hillelwayne.com/post/theorem-prover-showdown
--
-- Implemented using current stable-2.5 branch of Agda
-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude
-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94).

module Fulcrum where

open import Prelude hiding (_≤?_)

sjoerdvisscher

{-# LANGUAGE 
    TypeFamilies
  , KindSignatures
  , ScopedTypeVariables
  , ConstraintKinds
  , FlexibleInstances
  , FlexibleContexts
  , DeriveGeneric
  , DeriveAnyClass
  , TypeApplications

Blaisorblade

What I did to install Coq 8.8.1 with equations 1.1 as a separate profile:

opam switch coq-8.8.1 --alias-of 4.06.1
eval `opam config env`
opam pin add coq 8.8.1
opam pin add coq-equations 1.1+8.8
opam install ott coq-ott
(opam pin -y add coq-equations 1.1+8.8 && opam install -y ott coq-ott)

I lack notes, but you can repeat opam switch profileName --alias-of 4.06.1 more times

rntz

;; Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
#lang racket

;; Checks that a term has a type and returns its denotation.
(define (check cx tp-expect term)
  (match term
    [`(lambda (,x) ,body)
     (match-define `(-> ,A ,B) tp-expect)
     (define thunk (check (hash-set cx x A) B body))
     (lambda (env) (lambda (v) (thunk (hash-set env x v))))]

rntz

(* Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf *)
exception TypeError

type tp = Base | Fn of tp * tp
let subtype (x: tp) (y: tp): bool = x = y

type sym = {name: string; id: int}

let next_id = ref 0
let nextId() = let x = !next_id in next_id := x + 1; x