{{ message }}

Instantly share code, notes, and snippets.

# Larry Diehl larrytheliquid

Last active May 16, 2019
Run ghcid in a monorepo via stack
View stack-ghcid.sh
 project=\$(basename "\$(pwd)") # build dependencies build_deps="stack build \$project --fast --pedantic --dependencies-only --interleaved-output" # restart on changes in other packages restarts=\$(find ../. -maxdepth 1 -type d \ -not -name "\$project" \ -not -name .stack-work \ -not -name . \
Created Apr 27, 2018
Challenge 3 of the Great Theorem Prover Showdown
View Fulcrum.agda
 -- Problem 3 of @Hillelogram's Great Theorem Prover Showdown. -- https://www.hillelwayne.com/post/theorem-prover-showdown -- -- Implemented using current stable-2.5 branch of Agda -- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude -- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94). module Fulcrum where open import Prelude hiding (_≤?_)
Created Jan 6, 2017
View CoList.agda
 {-# 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
Created Oct 14, 2016
Type-safe printf, using runtime provided strings. An extension on https://gist.github.com/puffnfresh/11202637
View Main.idr
 module Main %default total data Format = FInt -- %d | FString -- %s | FOther Char -- [a-zA-Z0-9] format : List Char -> List Format
Last active Aug 3, 2017
A simple trick to pick a random element from a stream in constant memory
View PickRandom.hs
 {-# 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)
Created Aug 10, 2015
View fakechar.idr
 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
Last active May 31, 2019

Various blog posts related to Nix and NixOS

## General

Last active Jul 24, 2018
Simulating "type providers" in Agda
View RuntimeTypes.agda
 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
Last active Feb 10, 2021