{{ message }}

Instantly share code, notes, and snippets.

# Gergő Érdigergoerdi

Created Sep 5, 2010
View gist:566307
 1. clr z 2. jz a 7 3. dec a 4. inc z 5. inc b 6. jmp 2 7. jz z 11 8. dec z 9. inc a 10. jmp 7
Created Sep 6, 2010
View gist:567428
 ; program 9digits ; Register layout: ; ; n1-n9 the digits ; ; div the divisor to check ; ndiv n[div] ; k ; nk n[k] ;
Created Jun 3, 2012
The "MI to MU" puzzle from GEB
View MIU.agda
 module MIU where data Symbol : Set where I : Symbol U : Symbol open import Data.List Word : Set Word = List Symbol
Created Aug 17, 2012
Untyped lambda-calculus
View gist:3376887
 module Lambda where open import Data.Nat open import Data.Fin data Exp : ℕ → Set where Var : {n : ℕ} → Fin n → Exp n Lam : {n : ℕ} → Exp (suc n) → Exp n _·_ : {n m : ℕ} → Exp n → Exp m → Exp (n ⊓ m)
Created Aug 17, 2012
View gist:3376973
 {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} data Nat = Z | Suc Nat data Fin n where FZ :: Fin (Suc n) FS :: Fin n -> Fin (Suc n) inj :: Fin n -> Fin (Suc n) inj FZ = FZ
Created Oct 1, 2012
Using Tardis to turn generated names into nicely readable ones
 {-# LANGUAGE DataKinds, KindSignatures #-} {-# LANGUAGE GADTs, StandaloneDeriving #-} import Prelude hiding (mapM) import Data.Traversable (mapM) import Control.Monad.Tardis import Control.Monad.Free import Data.Stream (Stream(..)) import qualified Data.Stream as Stream import Data.Set (Set)
Created Apr 6, 2013
Trying to observe a difference between `pure id <*> x` and `x`
View gist:5324462
 import Control.Applicative.Free import Control.Applicative import Control.Monad.Identity import Data.Monoid count :: (Functor eff) => Free eff a -> Int count = getSum . runIdentity . analyze (const \$ Identity \$ Sum 1) test :: (Functor eff) => Free eff a -> (Int, Int)
Created Jul 3, 2013
Using SBV to break the hash described in http://twistedoakstudios.com/blog/Post4706_breaking-a-toy-hash-function
View gist:5917097
 -- http://twistedoakstudios.com/blog/Post4706_breaking-a-toy-hash-function import Data.List (findIndex) import Control.Monad (guard) import Data.Maybe (fromMaybe) import Data.SBV.Bridge.Boolector import Control.Monad.State import Control.Applicative codebook :: [Char]
Created Nov 27, 2014
http://mpickering.github.io/posts/2014-11-27-pain-free.html (take 2) that almost compiles
View Hutton2.hs
 {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-# LANGUAGE DeriveFunctor #-} newtype Fix f = Fix { unFix :: f (Fix f) } data HuttonF a = IntF Int | AddF a a deriving Functor type Hutton = Fix HuttonF
Created Nov 29, 2014
View families-closed.hs
 {- - Instant Insanity using Closed Type Families. - - See: http://stackoverflow.com/questions/26538595 -} {-# OPTIONS_GHC -ftype-function-depth=400 #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-}
You can’t perform that action at this time.