From dd0b1ecdbf2ea258a8255ea44c175b43c8623057 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Nov 2014 18:22:03 -0800 Subject: [PATCH] refactor(library/data/sigma): break file into smaller pieces to reduce dependencies --- library/data/sigma/decl.lean | 9 +++++++++ library/data/sigma/default.lean | 4 ++++ library/data/{sigma.lean => sigma/thms.lean} | 7 +------ 3 files changed, 14 insertions(+), 6 deletions(-) create mode 100644 library/data/sigma/decl.lean create mode 100644 library/data/sigma/default.lean rename library/data/{sigma.lean => sigma/thms.lean} (95%) diff --git a/library/data/sigma/decl.lean b/library/data/sigma/decl.lean new file mode 100644 index 000000000..eb7dc2477 --- /dev/null +++ b/library/data/sigma/decl.lean @@ -0,0 +1,9 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn +import logic.eq logic.heq data.unit + +structure sigma {A : Type} (B : A → Type) := +dpair :: (dpr1 : A) (dpr2 : B dpr1) + +notation `Σ` binders `,` r:(scoped P, sigma P) := r diff --git a/library/data/sigma/default.lean b/library/data/sigma/default.lean new file mode 100644 index 000000000..53f2d09ea --- /dev/null +++ b/library/data/sigma/default.lean @@ -0,0 +1,4 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn +import data.sigma.decl data.sigma.thms diff --git a/library/data/sigma.lean b/library/data/sigma/thms.lean similarity index 95% rename from library/data/sigma.lean rename to library/data/sigma/thms.lean index 4f79d2dff..8745615c3 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma/thms.lean @@ -1,14 +1,9 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -import logic.inhabited logic.cast +import data.sigma.decl open inhabited eq.ops -structure sigma {A : Type} (B : A → Type) := -dpair :: (dpr1 : A) (dpr2 : B dpr1) - -notation `Σ` binders `,` r:(scoped P, sigma P) := r - namespace sigma universe variables u v variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}