timjb

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

jonsterling

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,

callistabee

- Haskell Mergesort
- Copyright (C) 2014 by Kendall Stewart


First we define a couple of helper functions that
will be useful in splitting the list in half:

> fsthalf :: [a] -> [a]
> fsthalf xs = take (length xs `div` 2) xs

gitaarik

Git Submodules basic explanation

Why submodules?

In Git you can add a submodule to a repository. This is basically a repository embedded in your main repository. This can be very useful. A couple of usecases of submodules:

• Separate big codebases into multiple repositories.

copumpkin

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All

dmalikov

Various blog posts related to Nix and NixOS

---

General

• https://nixos.org/wiki/Main_Page Nix wiki. Awesome resource containing huge amount of manuals and documentation with examples.
• http://aflatter.de/nixos/ Alexander Flatter - NixOS. Installing NixOS inside a VirtualBox with a real-world configuration.nix example.
• http://lethalman.blogspot.it/search/label/nixpills Luca Bruno - Nix Pills. Series of posts describing how to install nix into some environment and how to use it.
• http://looprecur.com/blog/from-ubuntu-to-nixos/ Tim Sears - From Ubuntu to NixOS. Talk about experience migrating from Ubuntu to NixOS.

edwinb

data FakeChar = A | B | C
  
data ValidMyString : List Char -> Type where
     VA : ValidMyString xs -> ValidMyString ('a' :: xs)
     VB : ValidMyString xs -> ValidMyString ('b' :: xs)
     VC : ValidMyString xs -> ValidMyString ('c' :: xs)
     VNil : ValidMyString []
  
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
                      -> List FakeChar

jozefg

{-# LANGUAGE FlexibleContexts #-}
module PickRandom where
import Data.List (group, sort)
import Control.Monad
import Control.Monad.Random (MonadRandom, getRandomR)
import qualified Control.Foldl as F

-- Pick a value uniformly from a fold
pickRandom :: MonadRandom m => a -> F.FoldM m a a
pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst)

puffnfresh

module Main

%default total

data Format
  = FInt -- %d
  | FString -- %s
  | FOther Char -- [a-zA-Z0-9]

format : List Char -> List Format

larrytheliquid

{-# OPTIONS --copatterns #-}
module CoList where

{- High-level intuition:

codata CoList (A : Set) : Set where
  nil : CoList A
  cons : A → CoList A → CoList A

append : ∀{A} → CoList A → CoList A → CoList A