- All times will be communicated in a way that is unambiguous. This communication may be a local time, with a UTC offset specified.
For example:
Lysxia
/ functor.hs
Created
February 28, 2018 00:42
Deriving Functor instances in Haskell with GHC.Generics and one-liner
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
| -- Example of deriving Functor using GHC.Generics and one-liner with | |
| -- type-changing generic traversals. | |
| {-# LANGUAGE | |
| DeriveGeneric | |
| , DeriveFunctor | |
| , MonoLocalBinds -- TODO: used to turn off some warnings, why? | |
| , FlexibleContexts | |
| , TypeApplications | |
| , FlexibleInstances |
mpickering
/ Repro.hs
Created
February 27, 2018 15:42
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
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE | |
| DataKinds, | |
| TypeFamilies, | |
| TypeOperators, | |
| FlexibleContexts, | |
| TypeApplications, | |
| FlexibleInstances, | |
| AllowAmbiguousTypes, | |
| ScopedTypeVariables, |
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(timetop). | |
| -export([top/2]). | |
| top(Duration, Count) -> | |
| OldPrio = erlang:process_flag(priority, high), | |
| Result = scheduled_time_top(Duration), | |
| erlang:process_flag(priority, OldPrio), | |
| lists:sublist(Result, Count). |
fbettag
/ freebsd dalmatiner db 0.3.3 port - almost working
Created
November 15, 2017 05:50
Almost working port of dalmatinerdb. Works when you make package manually, but doesn't when poudriere tries to do offline/cleanroom builds. good luck, i'm out of time on this. HOW CAN A DATABASE CLAIM TO BE OPTIMIZED FOR ZFS AND NOT HAVE A WORKING FREEBSD PORT? WTF GUYS
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 a shell archive. Save it in a file, remove anything before | |
| # this line, and then unpack it by entering "sh file". Note, it may | |
| # create directories; files and directories will be owned by you and | |
| # have default permissions. | |
| # | |
| # This archive contains: | |
| # | |
| # databases | |
| # databases/dalmatinerdb | |
| # databases/dalmatinerdb/Makefile |
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
| Set Implicit Arguments. | |
| Inductive Place | |
| := Kitchen | Bedroom | Hallway | Outside. | |
| Inductive Card := NORTH | EAST | SOUTH | WEST. | |
| Definition moveTo (p : Place) (c : Card) : option Place := | |
| match p, c with |
anton-trunov
/ P1_valley.v
Created
May 18, 2017 11:13
Coq translation of a solution to the Valley Problem
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 a Coq translation of this solution: https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/mathprobs/p01.agda *) | |
| (* to this https://coq-math-problems.github.io/Problem1/ *) | |
| Require Import Coq.Arith.Arith. | |
| Definition decr (f : nat -> nat) := forall n, f (S n) <= f n. | |
| Definition n_valley n (f : nat -> nat) i := forall i', i' < n -> f (S (i' + i)) = f (i' + i). | |
| Lemma is_n_valley {f} n : decr f -> forall i, n_valley n f i \/ (exists i', f i' < f i). |
tonymorris
/ coc.md
Last active
March 9, 2022 11:34
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
| *.cm* | |
| /a.out |
chrisdone
/ FieldTH.hs
Last active
February 13, 2017 22:17
$(lens 'foo) -- handy one-off lens maker for record fields
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
| {-# LANGUAGE TemplateHaskell #-} | |
| -- | For when you have a record that doesn't have lenses derived for | |
| -- it and you need a lens, just use @$(lens 'thefield)@ and away you go. | |
| module Control.Lens.FieldTH where | |
| import Language.Haskell.TH | |
| lens :: Name -> Q Exp | |
| lens name = do | |
| [|\f r -> | |
| fmap | |
| $(lamE |
We can make this file beautiful and searchable if this error is corrected: It looks like row 5 should actually have 14 columns, instead of 6 in line 4.
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
| Name,Full name,Description,Location,Coordinates,URL,Version,DNSSEC validation,No logs,Namecoin,Resolver address,Provider name,Provider public key,Provider public key TXT record | |
| 4armed,4ARMED,DNSCrypt Server provided by www.4armed.com,France,,https://www.4armed.com,1,yes,yes,no,51.254.115.48:443,2.dnscrypt-cert.dnscrypt.4armed.io,FD3E:5887:63EA:17A9:1AF8:4325:DE82:1507:6ED0:01AB:2F9E:55DE:689B:F491:4D8E:526E, | |
| cisco,Cisco OpenDNS,Remove your DNS blind spot,Anycast,,https://www.opendns.com,1,no,no,no,208.67.220.220:443,2.dnscrypt-cert.opendns.com,B735:1140:206F:225D:3E2B:D822:D7FD:691E:A1C3:3CC8:D666:8D0C:BE04:BFAB:CA43:FB79, | |
| cisco-familyshield,Cisco OpenDNS with FamilyShield,Blocks web sites not suitable for children,Anycast,,https://www.opendns.com/home-internet-security/parental-controls/,1,no,no,no,208.67.220.123:443,2.dnscrypt-cert.opendns.com,B735:1140:206F:225D:3E2B:D822:D7FD:691E:A1C3:3CC8:D666:8D0C:BE04:BFAB:CA43:FB79, | |
| cisco-ipv6,Cisco OpenDNS over IPv6,Cisco OpenDNS IPv6 sandbox,Anycast,,https://www.op |