puffnfresh

module Reverse where

open import Data.List as List hiding (reverse)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where
  constructor rl
  field
    reverse0 : ∀ {A} → reverse {A} [] ≡ []

puffnfresh

import scala.language.higherKinds

trait Functor[F[_]] {
  def fmap[A, B](f: A => B): F[A] => F[B]
}

trait Apply[F[_]] {
  val functor: Functor[F]

  def ap[A, B](f: F[A => B]): F[A] => F[B]

puffnfresh

function some(a) {
    return {
        fold: function(f, _) {
            return f(a);
        },
        getOrElse: function(e) {
            return a;
        },
        orElse: function() {
            return some(a);

puffnfresh

package shajra.extn.scalaz.stream


import scalaz.{ Bind, Traverse, Unapply }
import scalaz.stream.Process


trait Syntax {

  implicit class ProcessSyntax[F[_], A](self: Process[F, A]) {

puffnfresh

let arrayMonad = {
  return: \x -> [x]
  bind: \x f -> Array.prototype.concat.apply [] (x.map f)
}

let array = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

console.log (do arrayMonad
  x <- array
  y <- array

puffnfresh

import language.implicitConversions

class AmbiguousStringAdd {
  def +(b: String) = ???
}

implicit def amb1any2stringadd(a: Any) = new AmbiguousStringAdd
implicit def amb2any2stringadd(a: Any) = new AmbiguousStringAdd

class A {}

puffnfresh

(function(global) {
    global.def = function define(name, dependencies, moduleFactory) {
        global.amdModules = global.amdModules || {};

        if (Object.prototype.toString.call(dependencies) != '[object Array]' && typeof dependencies !== 'function')
            throw new Error('dependencies must be an array. moduleFactory must be a function.');

        global.amdModules[name] = {
            'moduleFactory': moduleFactory || dependencies,
            'dependencies': typeof (moduleFactory) === 'undefined' ? [] : dependencies

puffnfresh

data GenericThing = SpecificThing Char | BadThing

isSpecificThing :: GenericThing -> Bool
isSpecificThing (SpecificThing _) = True
isSpecificThing _ = False

foo :: [GenericThing] -> GenericThing
foo xs
  | null xs                = error "Empty GenericThings"
  | all isSpecificThing xs = head xs

puffnfresh

module Main where

import Data.List (inits)
import Data.List.Split (splitOn)

main :: IO ()
main = print $ wordIndexes "Hello test  World"

wordIndexes :: String -> [(Int, String)]
wordIndexes s =

puffnfresh

module GCounter

import Data.Vect

||| GCounter is a Conflict Free Replicated Datatype.
||| For a definition, see https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type
||| It provides update, query and merge operations.
||| merge is commutative, associative and idempotent.
data GCounter : Nat -> Type where
  Nil : GCounter Z