Skip to content

Instantly share code, notes, and snippets.

rwbarton / eckmann_hilton.lean
Last active September 7, 2018 08:53 — forked from jcommelin/eckmann_hilton.lean
Eckmann—Hilton in Lean
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 / A.hs
Last active February 2, 2017 09:32 — forked from 23Skidoo/A.hs
-- Code taken from
-- Discussion on haskell-cafe:
-- 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)