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
\documentclass[11pt]{article} | |
\usepackage{fullpage} | |
\usepackage{amsmath} | |
\usepackage{amsfonts} | |
\usepackage{hyperref} | |
\newcommand{\RR}{\mathbb{R}} | |
\newcommand{\bool}{\mathtt{bool}} | |
\pagestyle{empty} |
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 tactic.interactive | |
universe u | |
namespace eckmann_hilton | |
variables (X : Type u) | |
local notation a `<`m`>` b := @has_mul.mul X m a b | |
class is_unital [m : has_mul X] [e : has_one X] : Prop := |
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
-- Code taken from http://stackoverflow.com/questions/12735274/breaking-data-set-integrity-without-generalizednewtypederiving/12744568#12744568 | |
-- Discussion on haskell-cafe: http://thread.gmane.org/gmane.comp.lang.haskell.cafe/100870 | |
-- http://www.haskell.org/pipermail/haskell-cafe/2012-October/103984.html | |
-- Modified to remove orphan instances by rwbarton | |
module A where | |
data U = X | Y deriving (Eq, Ord, Show) | |
data T u b c = T u b c deriving (Eq, Show) |
This file has been truncated, but you can view the full file.
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 644 reid6.ttyrec.bz2 | |
M0EIH.3%!629369%G\!P#EN/_____________________________________ | |
M________X5WCV<5..0````/OF`[L-N?=VZ'6YH79R<RT+M;G4IFUW=T+9$J2 | |
MKMIT`'RKK-@VU9'H!6V>C0.N>TGL8"O0/0`"CR!Z#0H=:#3()!LTJ]K8]H17 | |
M0=[V7<+,*"3652`2Z-=```9'*<Y9V[`DTH'1T5=6``T**`"NKO4C5`"@"@`` | |
M!T``Z]`#QA:)/B#[A0/0`HJI%V'TH!UT>AH='3=AW;)=F.[LZ+-:G7-U]"J& | |
M.FV!]`?3I-C&:SUU6^CO>X>>L;QY<&L`;IEP8`!W6XYG8R+@@`&YS.`P@`#= | |
MN[78;F``*8[-78``UTG,`&=6KI+NQQW=+3O/@`````````````!]```````` | |
M````-WJFX```#T````/H`%/H[Z\'`-```[email protected]@`:`````!][ZU3EE2,!AI0 | |
M)#I7VJ,F``&V`T`V"@Z4JI14*C0#@```#/K7MMM<-;8[-;/IZ-#T4>\#H`4* |
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
enum CHAR_ATTRIBUTES { | |
CHATTR_NORMAL = 0, | |
CHATTR_STANDOUT = 1, | |
CHATTR_BOLD = 2, | |
CHATTR_BLINK = 3, | |
CHATTR_UNDERLINE = 4, | |
CHATTR_REVERSE = 5, | |
CHATTR_DIM = 6, | |
CHATTR_HILITE = 7, | |
CHATTR_ATTRMASK = 15, |
This file has been truncated, but you can view the full file.
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
-- GENERATED by C->Haskell Compiler, version 0.16.4 Crystal Seed, 24 Jan 2009 (Haskell) | |
-- Edit the ORIGNAL .chs file instead! | |
{-# LINE 1 "enums.chs" #-}module Crawl.Enums where | |
data Crawl_CHAR_ATTRIBUTES = CHATTR_NORMAL | |
| CHATTR_STANDOUT | |
| CHATTR_BOLD | |
| CHATTR_BLINK | |
| CHATTR_UNDERLINE |