scott-fleischman

module VecList where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data List (A : Set) : Set where
  [] : List A
  _:>_ : A → List A → List A

data Vec (A : Set) : Nat → Set where

scott-fleischman

{-# OPTIONS --exact-split #-}

-- adapted from Greek Accents by D.A.Carson
module GreekAccents where

data Consonant : Set where
  β γ δ ζ θ κ ƛ μ ν ξ π ρ ῥ σ τ φ χ ψ [ : Consonant

data SingleVowel : Set where
  α ε η ι ο υ ω : SingleVowel

scott-fleischman

module Reify where

open import Agda.Builtin.Equality

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

module Function where

scott-fleischman

{-#  OPTIONS --type-in-type #-}

-- Taken from http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html

module _ where

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

data ⊥ : Set where

scott-fleischman

module Curry where

module And where

  data And : Set → Set → Set where
    and : (X Y : Set) → X → Y → And X Y

  curry
    : (X Y Z : Set)
    → (And X Y → Z)

scott-fleischman

module App.Todo where

import Prelude (const, (+), class Show, class Eq, eq, show, map, ($))
import Data.Array (snoc, filter)
import Pux.CSS (textDecoration, lineThrough, noneTextDecoration, style, TextDecoration, color, rgb)
import Pux.Html (Html, div, input, button, text, ul, li, p, a)
import Pux.Html.Attributes (type_, value, key)
import Pux.Html.Events (onChange, onClick)

data Action

scott-fleischman

module Set1

open MCPrelude

let fiveRands =
    let s0 = mkSeed 1I
    let (r1, s1) = rand s0
    let (r2, s2) = rand s1
    let (r3, s3) = rand s2
    let (r4, s4) = rand s3

scott-fleischman

{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE RebindableSyntax  #-}

module Set1 where

import MCPrelude

type Gen a = Seed -> (a, Seed)

fiveRands :: [Integer]

scott-fleischman

proof

cmp
  → {A : Set la} {B : Set lb} {C : Set lc}
  → (B → C)
  → (A → B)
  → (A → C)
cmp g f x = g (f x)

  pure a = a ∷ []

scott-fleischman

This 90-Day Plan Turns Engineers into Remarkable Managers

http://firstround.com/review/this-90-day-plan-turns-engineers-into-remarkable-managers/

On Code Review

http://glen.nu/ramblings/oncodereview.php