From 2b56a2b89109af02b2c8d3ffe5f158951951bebc Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 15 Dec 2014 16:43:42 -0500 Subject: [PATCH] feat(library/init): create markdown directory file --- library/init/default.lean | 1 + library/init/init.md | 44 ++++++++++++++++++++++++++++++++++++ library/init/measurable.lean | 3 +++ library/init/nat.lean | 2 ++ library/init/num.lean | 1 + library/init/priority.lean | 1 + library/init/prod.lean | 2 +- library/init/relation.lean | 2 ++ library/init/sigma.lean | 10 +++++--- library/init/tactic.lean | 1 + library/init/wf.lean | 2 ++ 11 files changed, 65 insertions(+), 4 deletions(-) create mode 100644 library/init/init.md diff --git a/library/init/default.lean b/library/init/default.lean index 28e21993e6..fd8425fd49 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -2,6 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Module: init.default Authors: Leonardo de Moura -/ prelude diff --git a/library/init/init.md b/library/init/init.md new file mode 100644 index 0000000000..ce5d86c8b0 --- /dev/null +++ b/library/init/init.md @@ -0,0 +1,44 @@ +init +==== + +The modules in this folder are required by low-level operations, and +are always imported by default. You can suppress this behavior by +beginning a file with the keyword "prelude". + +Syntax declarations: + +* [reserved_notation](reserved_notation.lean) +* [tactic](tactic.lean) +* [priority](priority.lean) + +Datatypes and logic: + +* [datatypes](datatypes.lean) +* [logic](logic.lean) +* [bool](bool.lean) +* [num](num.lean) +* [nat](nat.lean) + +Support for well-founded recursion: + +* [relation](relation.lean) +* [wf](wf.lean) +* [wf_k](wf_k.lean) +* [measurable](measurable.lean) + +Additional datatypes: + +* [prod](prod.lean) +* [sigma](sigma.lean) + +The default import: + +* [default](default.lean) + +Module init.logic defines "inhabited" and "nonempty" +types. Constructively, inhabited types have a witness, while nonempty +types are proof irrelevant. Classically (assuming the axioms in +logic.axioms.hilbert) the two are equivalent. Type class inferences +are set up to use "inhabited" however, so users should use that to +declare that types have an element. Use "nonempty" in the hypothesis +of a theorem when the theorem does not depend on the witness chosen. diff --git a/library/init/measurable.lean b/library/init/measurable.lean index 752a5e6180..93e5079ae4 100644 --- a/library/init/measurable.lean +++ b/library/init/measurable.lean @@ -2,7 +2,10 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Module: init.measurable Authors: Leonardo de Moura + +Types with a nat-valued complexity measure. -/ prelude import init.nat diff --git a/library/init/nat.lean b/library/init/nat.lean index 291eedbb4c..ee34238506 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -1,6 +1,8 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.nat Authors: Floris van Doorn, Leonardo de Moura -/ prelude diff --git a/library/init/num.lean b/library/init/num.lean index a3eed88bcd..f8a5172f90 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -2,6 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Module: init.num Authors: Leonardo de Moura -/ prelude diff --git a/library/init/priority.lean b/library/init/priority.lean index 8a23b06957..705ecd7796 100644 --- a/library/init/priority.lean +++ b/library/init/priority.lean @@ -2,6 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Module: init.priority Authors: Leonardo de Moura -/ prelude diff --git a/library/init/prod.lean b/library/init/prod.lean index d9bc84388c..ef2381b64c 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -2,7 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: data.prod.decl +Module: init.prod Author: Leonardo de Moura, Jeremy Avigad -/ prelude diff --git a/library/init/relation.lean b/library/init/relation.lean index 6774c6b7c2..059c361aad 100644 --- a/library/init/relation.lean +++ b/library/init/relation.lean @@ -1,6 +1,8 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module init.relation Authors: Leonardo de Moura -/ prelude diff --git a/library/init/sigma.lean b/library/init/sigma.lean index a3ac19c60b..e3c9adb9d0 100644 --- a/library/init/sigma.lean +++ b/library/init/sigma.lean @@ -1,6 +1,10 @@ --- 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 +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.sigma +Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn +-/ prelude import init.num init.wf init.logic init.tactic diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 27be915884..739731e0e7 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -2,6 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Module: init.tactic Author: Leonardo de Moura This is just a trick to embed the 'tactic language' as a Lean diff --git a/library/init/wf.lean b/library/init/wf.lean index db9d632b65..0dee4c7f38 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -1,6 +1,8 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.wf Author: Leonardo de Moura -/ prelude