michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/sigma): break file into smaller pieces to reduce dependencies

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-16 18:22:03 -08:00
parent e81d9c9184
commit dd0b1ecdbf
3 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/data/sigma/decl.lean Normal file
View file

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

4
library/data/sigma/default.lean Normal file
View file

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

7
library/data/sigma.lean → library/data/sigma/thms.lean
View file

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