Lizzie Dixon startling
startling
/ Recipes.hs
Created
July 5, 2013 05:54
This file contains 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 Control.Applicative.Recipes where | |
| -- base | |
| import Control.Applicative | |
| import Data.Foldable | |
| import Data.Traversable | |
| import Data.Monoid | |
| -- containers | |
| import Data.Set | |
| data Recipe k v m a = Recipe |
This file contains 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
| def bit_iter(bits, n): | |
| "Iterate over the bits of an integer, padding it to `n` digits." | |
| return ((bits >> i) & 1 for i in xrange(n - 1, -1, -1)) | |
| def unsigned_bin(x, n=32): | |
| "Print the unsigned binary representation of an integer." | |
| return "".join(repr(y) for y in bit_iter(x, n)) | |
| print unsigned_bin(0b101, 8) # '00000101' |
startling
/ impedimenta.hs
Created
April 9, 2013 01:00
This file contains 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
| import Sheets | |
| import Control.Applicative | |
| import Control.Monad.State | |
| import Data.Text (Text) | |
| import qualified Data.Text as T | |
| import qualified Data.Text.IO as T | |
| simple :: [T.Text] -> Table (State Int) Text | |
| simple = Table [counter id, see] |
This file contains 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
| data MaybeT : (Type -> Type) -> Type where | |
| MT : {m : Type -> Type} -> m (Maybe a) -> MaybeT m a |
startling
/ multidecorator.py
Last active
December 14, 2015 20:08
Multiple-argument decorators in python via classes!
This file contains 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
| def multidecorator(fn): | |
| class _MultiDecorator(object): | |
| class __metaclass__(type): | |
| def __new__(cls, name, bases, dict): | |
| # No magic on the first class with this metaclass | |
| if bases == (object,): | |
| return type.__new__(cls, fn.__name__, bases, dict) | |
| else: | |
| return fn(**dict) | |
| return _MultiDecorator |
startling
/ diagram.tex
Created
February 19, 2013 05:00
This file contains 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
| \begin{diagram} | |
| \named{a} \box \box \\ | |
| \box \box \named{b} \\ | |
| \box \box \empty | |
| \end{diagram} |
This file contains 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
| Elaborating {__Infer0} | |
| builtin:0 | |
| ---> Type a | |
| builtin:0:Constructor {__infer0} : {{A0} : Type} -> ({a0} : {A0}) -> {__Infer0} | |
| Rechecking ({A0} : Type 0) -> {A0} -> {__Infer0} | |
| ---> {__infer0} : ({A0} : Type c) -> {A0} -> {__Infer0} | |
| Forced: {__infer0} [] | |
| from ({A0} : Type c) -> {A0} -> {__Infer0} | |
| Elaborating {__Unit0} | |
| builtin:0 |
This file contains 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
| data Bool : Set where | |
| true : Bool | |
| false : Bool |
startling
/ ashkan.idr
Created
November 25, 2012 19:59
This file contains 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
| exp' : Nat -> Nat -> Nat | |
| exp' a b = a * a * (exp' a $ b - 1) | |
| ashkan : (a : Nat) -> (b : Nat) -> (c : Nat) -> (exp' a 2) + (exp' b 2) = (exp' c 2) -> Nat | |
| ashkan a b c = O |
startling
/ gist:4145092
Created
November 25, 2012 19:59
This file contains 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
| Can't unify Nat with (exp' a (fromInteger 2) + (exp' b (fromInteger 2)) = exp' c (fromInteger 2)) -> Nat | |
| Specifically: | |
| Can't unify Nat with (plus (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mult a a) (mult (mu |