I hereby claim:
- I am aspiwack on github.
- I am aspiwack (https://keybase.io/aspiwack) on keybase.
- I have a public key ASAdUTbPKE_sXn1PUR6IItRsYY6oaQki2LSvqSdZsCkntgo
To claim this, I am signing this object:
package util | |
import scala.reflect.ClassTag | |
sealed abstract class Diffed[+A] | |
final case class Unchanged[+A](x: A) extends Diffed[A] { | |
override def toString: String = "Unchanged(" + x + ")" | |
} | |
final case class Changed[+A](x: A) extends Diffed[A] { | |
override def toString: String = "Changed(" + x + ")" |
(** To give a direct proof of the constructive result that [forall | |
A:Prop, ~~(A\/~A)], it is useful to see [~A] as meaning a | |
"continuation of [A]". That is, [~A] is a computation that takes an | |
[A] and "returns".*) | |
(** Here is a first proof by forward chaining. *) | |
Lemma Proof₁ : forall A:Prop, ~~(A\/~A). | |
Proof. | |
intros A k₀. | |
(** We have [k₀:~(A\/~A)]. That is [k₀] is a continuation of either |
PKG core_bench | |
PKG qcheck | |
B _build |
(** A small STG-like lazy abstract machine. What I take from the STG | |
is that constructors are responsible for choosing a branch in a | |
pattern-matching (the T in STG) and for updating themselves (by | |
pushing an update frame). Apart from that it's not very different | |
from a simple KAM. Note that the current implementation in GHC is | |
not actually tagless anymore, as it proved to be slower than a | |
tagged mechanism. But since it's a simpler design, (and the | |
difference doesn't matter much unless actual machine code is | |
emitted). |
I hereby claim:
To claim this, I am signing this object:
;; I wrote a bit of Emacs configuration (which can be added to your | |
;; init.el) so that an lhs2tex file can be syntax-highlighted as a | |
;; Latex file but the Haskell code is highlighted as Haskell code. In | |
;; fact it's a little more than this, as the code blocks are | |
;; interpreted with the haskell-mode, so you can use your haskell | |
;; commands there. | |
;; | |
;; I don't recommend opening all `.lhs' file in this mode, as they | |
;; don't need to be Latex files. Literate Haskell is really agnostic | |
;; about its surrounding language. |
Ubuntu 21.04 comes with Pipewire pre-installed. A pipewire service is
running, but it’s doesn’t handle audio by default. For this you need
to install a pipewire-pulse
service. The (preinstalled) pipewire
package provides such a service as documentation. First let’s copy it
in Systemd’s space.
$ cp /usr/share/doc/pipewire/examples/systemd/user/pipewire-pulse.* /usr/lib/systemd/user/
module CatList : sig | |
(** “Lazy” lists with O(1) concatenation. *) | |
type +'a t | |
type (+'a, +'l) view = | |
| Nil | |
| Cons of 'a * 'l | |
val view : 'a t -> ('a, 'a t) view |
module Cdcl where | |
import Data.Foldable | |
import Data.Maybe | |
import Data.Monoid | |
type Atom = Int | |
type Literal = (Bool, Atom) |