Mercerenies

-- Haskell program which generates the table

import Data.Ratio
import Data.List

divides :: Integral a => a -> a -> Bool
divides y x = x `mod` y == 0

primeFactors :: Integral a => a -> [a]
primeFactors n | n < 1 = error "invalid input"

Mercerenies

;; manual

10000 times {
  a := 1.
  a= := { parent a := #'($1). }.
  do { a = 2. }.
}.

;; assignable

Mercerenies

import java.util.ArrayList;
import java.util.Collection;

public class CollRaw {

  public static interface Test {
    public StringBuilder append(Collection<?> value);
  }

Mercerenies

-- Note: The same warnings about ListT's poor behavior apply to this transformer.
-- https://wiki.haskell.org/ListT_done_right

import Data.List.NonEmpty
import Control.Monad
import Control.Monad.List

newtype NonEmptyT m a = NonEmptyT { unNonEmptyT :: m (NonEmpty a) }

Mercerenies

open import Agda.Builtin.Equality

record _∧_ (A B : Set) : Set where
  constructor conj
  field
    proj₁ : A
    proj₂ : B

data List (A : Set) : Set where