luksamuk

∇R←IDENTITY N
  R←(N N)⍴(1,N⍴0)
∇

∇R←EXTENDBOTTOM MAT
  R←(((↑⍴MAT)⍴1),0)\[1]MAT
∇

∇R←EXTENDRIGHT MAT
  R←(((2⌷⍴MAT)⍴1),0)\MAT

enobayram

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

// return :: Monad m => a -> m a
typedef void * /* m a */ return_t(void * /* a */);

// type kleisli_arrow a b = a -> m b
typedef void * /* m b */ kleisli_arrow(void * /* a */);

// bind :: Monad m => m a -> (a -> m b) -> m b

rizo

#include <iostream>
#include <assert.h>
#include <forward_list>
#include <functional>


template <typename T>
struct option {
public:
  class no_value { };

takada-at

-- definition of Existential Type
data ∃ {A : Set} (B : A → Set) : Set where
     _,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x


-- left projection
p : {A : Set} {B : A → Set} → (∃ \(x : A) → B x) → A
p {A} {B} (a , b) = a

-- right projection

machuidel

#pragma once

#ifndef _XOPTION_TYPE_H_
#define _XOPTION_TYPE_H_

#ifdef __cplusplus
extern "C"
{
#endif

poizan42

Require Import Coq.ZArith.ZArith.
Require Import Coq.ZArith.Znumtheory.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Coq.PArith.BinPos.

Definition Z_ens := Ensemble Z.
Print Finite.
Print Empty_set.
Definition is_empty_set U A := forall x, ~(In U A x).

Kimundi

Introduction

If you are familiar with Java's generics, and are coming to Rust, you might be lead to assume that its generics are working the same way.

However, due to the different type systems, and different implementation details, there are quite a few differences between generic code in both languages.

This document tries to give a short summary about those differences:

Core functionality

Java

splinterofchaos

#include <memory>
#include <iostream>
#include <sstream>
#include <utility>
#include <algorithm>
#include <iterator>

struct sequence_tag {};
struct pointer_tag {};

tarao

namespace lambda {

////////////////////////////////////////////////
// Lambda term

namespace term {

template<char c> struct var {};
template<typename N, typename M> struct app {};
template<char v, typename M> struct abs {};