rwbarton

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{hyperref}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\bool}{\mathtt{bool}}

\pagestyle{empty}

rwbarton

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 :=

rwbarton

-- 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)

rwbarton

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\'`-```=.@.B@`:`````!][ZU3EE2,!AI0
M)#I7VJ,F``&V`T`V"@Z4JI14*C0#@```#/K7MMM<-;8[-;/IZ-#T4>\#H`4*

rwbarton

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,

rwbarton

-- 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