Skip to content

Instantly share code, notes, and snippets.

Josh Tilles MerelyAPseudonym

Block or report user

Report or block MerelyAPseudonym

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@cyriux
cyriux / ModelingMusicDDDPractitioner.md
Last active Oct 3, 2019
Links of the talk Modeling Music for DDD Practitioner
View ModelingMusicDDDPractitioner.md
View _carry.md

Carry

Frequently I want to use reductions only to quickly realize that I'm not interested in the successive values of the state.

A simple example is to imagine one wants to increment a number represented by a sequence of its binary digits:

(inc '()) is (1)
(inc '(1)) is (0 1) ; yes the list is inversed, the lowest significant bit is the first item
(inc '(0 1)) is (1 1)
@kachayev
kachayev / aleph-planning.md
Last active Sep 9, 2019
A few thoughts on Aleph development
View aleph-planning.md

Aleph, Async, HTTP, Clojure

I've been working with Aleph rougly for last 5 years, actively contributing to the library for last 2 (or so). I also put some effort into spreading the word about it, including educational tech talks, like "Deep HTTP Dive Throught Aleph & Netty". But the more I talk to people the more confusion I find, mostly about how Aleph works and what can you expect when adding it to your stack. Clojurists Together has recently announced Aleph to get Q1 funding, I think it's a good time to share my priorities and thoughts on development plans that were mentioned in the blog post. Hope the community would find it interesting and helpful.

Aleph describes itself as "asynchronous communication for Clojure" library. And you should probably pay a good portion of your attention to the first word: "asynchronous".

View nix-flakes.md

Nix Flake MVP

Goals

  • To provide Nix repositories with an easy and standard way to reference other Nix repositories.

  • To allow such references to be queried and updated automatically.

  • To provide a replacement for nix-channel, NIX_PATH and Hydra

@parsonsmatt
parsonsmatt / prismatic.hs
Created Jun 5, 2018
I figured out a nice way to pluck exceptions out of a constraint!
View prismatic.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
@Rotsor
Rotsor / fulcrum.lean
Last active May 15, 2018
Fulcrum in lean
View fulcrum.lean
-- Solution for the "Fulcrum" problem from "The Great Theorem Prover Showdown"
-- (https://www.hillelwayne.com/post/theorem-prover-showdown/)
--
-- I am novice with Lean so the verbosity is almost certainly my
-- fault and not that of Lean.
import system.io
universes u v w
-----------------------------------------
@mfikes
mfikes / lein-tools-deps-cursive.md
Last active Oct 9, 2018
Using `lein-tools-deps` from Cursive (on macOS)
View lein-tools-deps-cursive.md

Note: These workarounds covered issues in lein-tools-deps 0.3.0-SNAPSHOT. If using 0.4.1 or later, you should not encounter the issues below.

The following provides some workarounds for some issues when using lein-tools-deps from Cursive on macOS.

Path to clojure

By default, the lein-tools-deps plugin won't see /usr/local/bin/clojure when Cursive processes project.clj, as it evidently has a degenerate path.

You will see an error like the following in the IntelliJ Event Log when it tries to process your project.clj file:

@vvvvalvalval
vvvvalvalval / datomic-erasing-data-migration.clj
Created Apr 25, 2018
Erasing data from Datomic via a manual data migration
View datomic-erasing-data-migration.clj
;; # EMULATING DATOMIC EXCISION VIA MANUAL DATA MIGRATION
;; *************************************
;; ## Introduction
;; *************************************
;; This Gist demonstrates a generic way to migrate an entire Datomic database
;; from an existing 'Origin Connection' to a clean 'Destination Connection',
;; while getting rid of some undesirable data and otherwise preserving history.
@porglezomp
porglezomp / Leftpad.idr
Last active Oct 22, 2018
Taking on Hillel's challenge to formally verify leftpad (https://twitter.com/Hillelogram/status/987432181889994759)
View Leftpad.idr
import Data.Vect
-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max Z (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl
-- The type here says "the result is" padded to (maximum k n), and is padding plus the original
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)
You can’t perform that action at this time.