| module Cdcl where | |
| import Data.Foldable | |
| import Data.Maybe | |
| import Data.Monoid | |
| type Atom = Int | |
| type Literal = (Bool, Atom) |
| 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 |
| ;; 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/| PKG core_bench | |
| PKG qcheck | |
| B _build |
| type void = { ex_falso : 'a.'a } | |
| module Eq = struct | |
| (** Leibniz equality. *) | |
| type (_,_) t = Refl : ('a,'a) t | |
| (** Variant of equality with a dummy case used to prove disequalities. *) | |
| type (_,_) u = Refl' : ('a,'a) u | Dummy : void -> ('a,'b) u |
I hereby claim:
To claim this, I am signing this object:
| (** 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). |
| (** 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 |
| (** In this file we go a little further and follow the derivation | |
| proposed by Jeremy Gibbons ( | |
| http://patternsinfp.wordpress.com/2011/05/05/horners-rule/ ). It | |
| uses the definitions in Scan.v. The problem is to compute the | |
| maximum sum of consecutive elements in a list [l]. It happens that | |
| there is a linear time solution for that problem. Again, we start | |
| with a simple executable specification, and using appropriate | |
| rewriting steps, we find the linear time solution. *) | |
| Require Import Prelim List NList Scan. |