co-dan

>     modifyMatch :: LMatch RdrName (LHsExpr RdrName)
>                 -> LMatch RdrName (LHsExpr RdrName)
>     modifyMatch (L l1 (Match lpat lty rs@(GRHSs{..}))) =
>         let f (L l1 (GRHS guards body)) =
>                 L l1 (GRHS guards (modifyExpr body))
>         in L l1 (Match lpat lty (rs
>                                  { grhssGRHSs = map f grhssGRHSs }))

co-dan

/* FNV-1 hash
*
* The FNV-1 hash description: http://isthe.com/chongo/tech/comp/fnv/
* The FNV-1 hash is public domain: http://isthe.com/chongo/tech/comp/fnv/#public_domain

long hashable_fnv_hash(const unsigned char* str, long len, long hash) {

  while (len--) {
    hash = (hash * 16777619) ^ *str++;
  }

co-dan

{-# LANGUAGE TypeFamilies,
             MultiParamTypeClasses,
             FlexibleInstances,
             UndecidableInstances,
             FunctionalDependencies #-}

import Control.Concurrent
import Control.Monad
import Control.Monad.Fix
import JavaScript.JQuery

co-dan

Resolving dependencies...
Configuring diagrams-contrib-1.0.0.1...
Building diagrams-contrib-1.0.0.1...
Preprocessing library diagrams-contrib-1.0.0.1...

src/Diagrams/TwoD/Tilings.hs:94:39:
     warning: missing terminating ' character [-Winvalid-pp-token]
-- Instead of using Doubles, which can't be compared for equality, it
                                      ^

co-dan

#
# This simple script displays whether you are in a cabal sandbox
# the the result of checking for a sandbox is cached, but now that I
# actually think about it, it was probably an unnecessary step.
# Don't forget to customize the PROMPT variable at the bottom 
#
# Looks like this with my prompt: https://files.app.net/rjphjAG9.png
#

function update_cabal_sandbox_info () {

co-dan

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module SeqFoldable where

import           Prelude hiding (drop, take)

import           Data.Functor.Foldable
import           Data.Sequence         (Seq, ViewL (..), (<|))
import qualified Data.Sequence         as S

co-dan

--------------------------------------------------
-- Yoneda lemma

newtype Yoneda f a =
    Yoneda (forall b. (a -> b) -> f b)
    -- Nat (Hom(a, -), F) ~~ F a
    
-- this is `liftYoneda`
yoneda :: (Functor f) => f a -> Yoneda f a
yoneda x = Yoneda $ \f -> fmap f x

co-dan

{-# LANGUAGE OverloadedStrings #-}

module Controllers.Home (homeRoutes) where

import Web.Scotty
import Data.Monoid                              (mconcat)
import qualified Database.RethinkDB as R
import qualified Database.RethinkDB.NoClash

homeRoutes :: ScottyM ()

co-dan

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
         (f0 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (3+m) (g_plus3 m e)) 
         (f1 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (5+m) (g_plus5 m e)) 
         (n : nat) (e: gorgeous n) : P n e :=

co-dan

Require Import Rel.
Require Import Coq.Init.Wf.

Theorem nat_wo: well_founded lt.
Proof.
  intro n.
  assert (forall y x, x < y -> Acc lt x) as A.
  induction y.
  + intros x H; inversion H.
  + intros x H'. apply Acc_intro.