staltz

The introduction to Reactive Programming you've been missing

(by @andrestaltz)

---

This tutorial as a series of videos

If you prefer to watch video tutorials with live-coding, then check out this series I recorded with the same contents as in this article: Egghead.io - Introduction to Reactive Programming.

---

lelandbatey

Description

This simple script will take a picture of a whiteboard and use parts of the ImageMagick library with sane defaults to clean it up tremendously.

The script is here:

#!/bin/bash
convert "$1" -morphology Convolve DoG:15,100,0 -negate -normalize -blur 0x1 -channel RBG -level 60%,91%,0.1 "$2"

Results

malarkey

When times get tough and people get nasty, you’ll need more than a killer smile. You’ll need a killer contract.

Used by 1000s of designers and developers Clarify what’s expected on both sides Helps build great relationships between you and your clients Plain and simple, no legal jargon Customisable to suit your business Used on countless web projects since 2008

…………………………

grugq

Simple Security Guidelines

Using an iDevice? (Best option)

• Use an iPod or an iPad without a SIM card
• Use an iPhone
• Do not jailbreak
• Always upgrade to new iOS versions
• Use Brave browser

Need Secure chat?

chrisdone

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions:

gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

andrejbauer

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection

copumpkin

module Prime where

open import Coinduction

open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
open import Data.Fin.Props hiding (_≟_)

grownseed

Give me back my sanity

One of the many things I do for my group at work is to take care of automating as many things as possible. It usually brings me a lot of satisfaction, mostly because I get a kick out of making people's lives easier.

But sometimes, maybe too often, I end up in drawn-out struggles with machines and programs. And sometimes, these struggles bring me to the edge of despair, so much so that I regularly consider living on a computer-less island growing vegetables for a living.

This is the story of how I had to install Pandoc in a CentOS 6 Docker container. But more generally, this is the story of how I think computing is inherently broken, how programmers (myself included) tend to think that their way is the way, how we're ultimately replicating what most of us think is wrong with society, building upon layers and layers of (best-case scenario) obscure and/or weak foundations.

*I would like to extend my gratitude to Google, StackOverflow, GitHub issues but mostly, the people who make the