Skip to content

Instantly share code, notes, and snippets.

View relrod's full-sized avatar

Rick Elrod relrod

291 followers · 398 following
View GitHub Profile
@relrod
relrod / topology.v
Created May 15, 2016 08:24 — forked from andrejbauer/topology.v
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
*)
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.
@relrod
relrod / stickers.md
Last active April 23, 2016 20:06
Functional Programming Stickers
@relrod
relrod / group_theory.v
Last active April 7, 2016 03:18
Playing with formalizing some stuff from Abstract Algebra in Coq.
(* This is just something I started playing around with. *)
(* The proofs are probably very inefficient and bad. *)
(* Next steps are to be more pedantically accurate in the hierarchy (e.g. *)
(* semigroup, magma, etc.) and also begin formalizing subgroups. *)
(* If I keep having fun, I might start on formalizing some category theory *)
(* stuff as I go, too. *)
Require Import ZArith.
Require Import String.
Require Import Basics.
@relrod
relrod / Approach1.hs
Created January 12, 2016 21:59
What is the practical difference?
module Approach1 where
import Control.Applicative
import Control.Monad
import Prelude (Functor, Char, fmap, (.), IO)
import qualified Prelude
data IOOperation a =
PutChar Char a
| GetChar (Char -> a)
@relrod
relrod / gist:216b6da945344972fc36
Created January 6, 2016 13:47
ricky@monadic ⚡96% /tmp/s$ pulp
module.js:328
throw err;
^
Error: Cannot find module './pulp'
at Function.Module._resolveFilename (module.js:326:15)
at Function.Module._load (module.js:277:25)
at Module.require (module.js:354:17)
at require (internal/module.js:12:17)
@relrod
relrod / fen.hs
Created December 18, 2015 00:33
λ> let Right x = parseOnly parseRanks "rnbqkbnr/pppppppp/8/8/8/8/PPPPPPPP/RNBQKBNR"
x :: [Cell]
λ> putStrLn $ prettyPrintBoard x ""
♜ ♞ ♝ ♛ ♚ ♝ ♞ ♜
♟ ♟ ♟ ♟ ♟ ♟ ♟ ♟
♙ ♙ ♙ ♙ ♙ ♙ ♙ ♙
@relrod
relrod / challenge.hs
Created December 5, 2015 19:31
a 0 = 1
a 1 = 2
a n = (4 * (a (n - 1))) - (a (n - 2))
-- what is: a 2015
@relrod
relrod / Free.fr
Last active December 2, 2015 18:57
module hello.HelloWorld where
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
data Free f a = Pure a | Free (f (Free f a))
liftF :: Functor f => f a -> Free f a
liftF f = Free (fmap Pure f)
@relrod
relrod / gist:55e7276f4ca433a8a6f0
Created October 28, 2015 04:26
systemd, what are you even doing
Oct 28 00:12:05 t520 journal: Permanent journal (/var/log/journal/) is currently using 4.0G.#012Maximum allowed usage is set to 4.0G.#012Leaving at least 4.0G free (of currently available 7.6G of space).#012Enforced usage limit is thus 4.0G.
Oct 28 00:12:05 t520 journal: Journal started
Oct 28 00:12:05 t520 kernel: ata1.00: exception Emask 0x0 SAct 0x0 SErr 0x50000 action 0x6 frozen
Oct 28 00:12:05 t520 kernel: ata1: SError: { PHYRdyChg CommWake }
Oct 28 00:12:05 t520 kernel: ata1.00: failed command: FLUSH CACHE EXT
Oct 28 00:12:05 t520 kernel: ata1.00: cmd ea/00:00:00:00:00/00:00:00:00:00/a0 tag 28#012 res 40/00:01:00:00:00/00:00:00:00:00/e0 Emask 0x4 (timeout)
Oct 28 00:12:05 t520 kernel: ata1.00: status: { DRDY }
Oct 28 00:12:05 t520 kernel: ata1: hard resetting link
Oct 28 00:12:05 t520 kernel: ata1: SATA link up 6.0 Gbps (SStatus 133 SControl 300)
Oct 28 00:12:05 t520 kernel: ata1.00: ACPI cmd f5/00:00:00:00:00:a0 (SECURITY FREEZE LOCK) filtered out
@relrod
relrod / gist:6ffb71987977630cd9d6
Created October 13, 2015 01:38
Can we have working software yet? Please?
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE)
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) Backtrace:
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 0: /usr/libexec/Xorg (?+0x0) [0x59a350]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 1: /lib64/libc.so.6 (?+0x0) [0x3d5dc34a4f]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 2: /usr/lib64/xorg/modules/drivers/intel_drv.so (?+0x0) [0x7fa39aae0c80]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 3: /usr/lib64/xorg/modules/drivers/intel_drv.so (?+0x0) [0x7fa39ab16620]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 4: /usr/libexec/Xorg (?+0x0) [0x43eeb0]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 5: /usr/libexec/Xorg (?+0x0) [0x5931b0]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 6: /usr/libexec/Xorg (?+0x0) [0x43a200]
Oct 12 21:17:21 t520 /usr/libexec/gdm-x-session: (EE) 7: /usr/libexec/Xorg (?+0x0) [0x43e1e0]