A list of Functional Programming related sticker goodness for your laptop!
Rick Elrod 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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* 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
/ group_theory.v
Last active
April 7, 2016 03:18
Playing with formalizing some stuff from Abstract Algebra in Coq.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* 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. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ gist:216b6da945344972fc36
Created
January 6, 2016 13:47
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| λ> let Right x = parseOnly parseRanks "rnbqkbnr/pppppppp/8/8/8/8/PPPPPPPP/RNBQKBNR" | |
| x :: [Cell] | |
| λ> putStrLn $ prettyPrintBoard x "" | |
| ♜ ♞ ♝ ♛ ♚ ♝ ♞ ♜ | |
| ♟ ♟ ♟ ♟ ♟ ♟ ♟ ♟ | |
| ♙ ♙ ♙ ♙ ♙ ♙ ♙ ♙ |
relrod
/ challenge.hs
Created
December 5, 2015 19:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| a 0 = 1 | |
| a 1 = 2 | |
| a n = (4 * (a (n - 1))) - (a (n - 2)) | |
| -- what is: a 2015 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ gist:6ffb71987977630cd9d6
Created
October 13, 2015 01:38
Can we have working software yet? Please?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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] |